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

Theorem vtocl2g 3259
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 2761 . 2 𝑥𝐴
2 nfcv 2761 . 2 𝑦𝐴
3 nfcv 2761 . 2 𝑦𝐵
4 nfv 1840 . 2 𝑥𝜓
5 nfv 1840 . 2 𝑦𝜒
6 vtocl2g.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
7 vtocl2g.2 . 2 (𝑦 = 𝐵 → (𝜓𝜒))
8 vtocl2g.3 . 2 𝜑
91, 2, 3, 4, 5, 6, 7, 8vtocl2gf 3257 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 3191
This theorem is referenced by:  vtocl4g  3266  ifexg  4134  uniprg  4421  intprg  4481  opthg  4911  opelopabsb  4950  vtoclr  5129  elimasng  5455  cnvsng  5585  funopg  5885  f1osng  6139  fsng  6364  fvsng  6407  fnpr2g  6434  unexb  6918  op1stg  7132  op2ndg  7133  xpsneng  7997  xpcomeng  8004  sbth  8032  unxpdom  8119  fpwwe2lem5  9408  prcdnq  9767  mhmlem  17467  carsgmon  30181  br1steqg  31411  br2ndeqg  31412  brimageg  31711  brdomaing  31719  brrangeg  31720  rankung  31950  mbfresfi  33123  zindbi  37026  2sbc6g  38133  2sbc5g  38134  fmulcl  39245
  Copyright terms: Public domain W3C validator