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

Theorem vtocl2ga 3264
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 2761 . 2 𝑥𝐴
2 nfcv 2761 . 2 𝑦𝐴
3 nfcv 2761 . 2 𝑦𝐵
4 nfv 1840 . 2 𝑥𝜓
5 nfv 1840 . 2 𝑦𝜒
6 vtocl2ga.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
7 vtocl2ga.2 . 2 (𝑦 = 𝐵 → (𝜓𝜒))
8 vtocl2ga.3 . 2 ((𝑥𝐶𝑦𝐷) → 𝜑)
91, 2, 3, 4, 5, 6, 7, 8vtocl2gaf 3263 1 ((𝐴𝐶𝐵𝐷) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192
This theorem is referenced by:  solin  5028  caovcan  6803  pwfseqlem2  9441  mulcanenq  9742  ltaddnq  9756  ltrnq  9761  genpv  9781  wrdind  13430  fsumrelem  14485  imasleval  16141  fullfunc  16506  fthfunc  16507  pf1ind  19659  mretopd  20836  dvlip  23694  scvxcvx  24646  issubgoilem  28005  cnre2csqlem  29780
  Copyright terms: Public domain W3C validator