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

Theorem vtocl2g 3421
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 2913 . 2 𝑥𝐴
2 nfcv 2913 . 2 𝑦𝐴
3 nfcv 2913 . 2 𝑦𝐵
4 nfv 1995 . 2 𝑥𝜓
5 nfv 1995 . 2 𝑦𝜒
6 vtocl2g.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
7 vtocl2g.2 . 2 (𝑦 = 𝐵 → (𝜓𝜒))
8 vtocl2g.3 . 2 𝜑
91, 2, 3, 4, 5, 6, 7, 8vtocl2gf 3419 1 ((𝐴𝑉𝐵𝑊) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353
This theorem is referenced by:  vtocl4g  3428  ifexg  4296  uniprg  4588  intprg  4645  opthg  5073  opelopabsb  5118  vtoclr  5304  elimasng  5632  cnvsngOLD  5765  funopg  6065  f1osng  6318  fsng  6547  fvsng  6591  fnpr2g  6618  unexb  7105  op1stg  7327  op2ndg  7328  xpsneng  8201  xpcomeng  8208  sbth  8236  unxpdom  8323  fpwwe2lem5  9658  prcdnq  10017  mhmlem  17743  carsgmon  30716  br1steqgOLD  32010  br2ndeqgOLD  32011  brimageg  32371  brdomaing  32379  brrangeg  32380  rankung  32610  mbfresfi  33788  zindbi  38037  2sbc6g  39142  2sbc5g  39143  fmulcl  40331
  Copyright terms: Public domain W3C validator