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

Theorem vtocl2g 3243
 Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.)
Hypotheses
Ref Expression
vtocl2g.1 (𝑥 = 𝐴 → (𝜑𝜓))
vtocl2g.2 (𝑦 = 𝐵 → (𝜓𝜒))
vtocl2g.3 𝜑
Assertion
Ref Expression
vtocl2g ((𝐴𝑉𝐵𝑊) → 𝜒)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑦,𝐵   𝜓,𝑥   𝜒,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝜒(𝑥)   𝐵(𝑥)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem vtocl2g
StepHypRef Expression
1 nfcv 2751 . 2 𝑥𝐴
2 nfcv 2751 . 2 𝑦𝐴
3 nfcv 2751 . 2 𝑦𝐵
4 nfv 1830 . 2 𝑥𝜓
5 nfv 1830 . 2 𝑦𝜒
6 vtocl2g.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
7 vtocl2g.2 . 2 (𝑦 = 𝐵 → (𝜓𝜒))
8 vtocl2g.3 . 2 𝜑
91, 2, 3, 4, 5, 6, 7, 8vtocl2gf 3241 1 ((𝐴𝑉𝐵𝑊) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175 This theorem is referenced by:  vtocl4g  3250  ifexg  4107  uniprg  4386  intprg  4446  opthg  4872  opelopabsb  4910  vtoclr  5086  elimasng  5410  cnvsng  5539  funopg  5836  f1osng  6089  fsng  6310  fvsng  6352  fnpr2g  6379  unexb  6856  op1stg  7071  op2ndg  7072  xpsneng  7930  xpcomeng  7937  sbth  7965  unxpdom  8052  fpwwe2lem5  9335  prcdnq  9694  mhmlem  17358  2pthoncl  26133  carsgmon  29703  br1steqg  30919  br2ndeqg  30920  brimageg  31204  brdomaing  31212  brrangeg  31213  rankung  31443  mbfresfi  32626  zindbi  36529  2sbc6g  37638  2sbc5g  37639  fmulcl  38648
 Copyright terms: Public domain W3C validator