Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtocl2ga Structured version   Visualization version   GIF version

Theorem vtocl2ga 3402
 Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.)
Hypotheses
Ref Expression
vtocl2ga.1 (𝑥 = 𝐴 → (𝜑𝜓))
vtocl2ga.2 (𝑦 = 𝐵 → (𝜓𝜒))
vtocl2ga.3 ((𝑥𝐶𝑦𝐷) → 𝜑)
Assertion
Ref Expression
vtocl2ga ((𝐴𝐶𝐵𝐷) → 𝜒)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝜓,𝑥   𝜒,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝜒(𝑥)   𝐵(𝑥)

Proof of Theorem vtocl2ga
StepHypRef Expression
1 nfcv 2890 . 2 𝑥𝐴
2 nfcv 2890 . 2 𝑦𝐴
3 nfcv 2890 . 2 𝑦𝐵
4 nfv 1980 . 2 𝑥𝜓
5 nfv 1980 . 2 𝑦𝜒
6 vtocl2ga.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
7 vtocl2ga.2 . 2 (𝑦 = 𝐵 → (𝜓𝜒))
8 vtocl2ga.3 . 2 ((𝑥𝐶𝑦𝐷) → 𝜑)
91, 2, 3, 4, 5, 6, 7, 8vtocl2gaf 3401 1 ((𝐴𝐶𝐵𝐷) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1620   ∈ wcel 2127 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330 This theorem is referenced by:  solin  5198  caovcan  6991  pwfseqlem2  9644  mulcanenq  9945  ltaddnq  9959  ltrnq  9964  genpv  9984  wrdind  13647  fsumrelem  14709  imasleval  16374  fullfunc  16738  fthfunc  16739  pf1ind  19892  mretopd  21069  dvlip  23926  scvxcvx  24882  issubgoilem  28397  cnre2csqlem  30236
 Copyright terms: Public domain W3C validator