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

Theorem vtocl2g 3402
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 2894 . 2 𝑥𝐴
2 nfcv 2894 . 2 𝑦𝐴
3 nfcv 2894 . 2 𝑦𝐵
4 nfv 1984 . 2 𝑥𝜓
5 nfv 1984 . 2 𝑦𝜒
6 vtocl2g.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
7 vtocl2g.2 . 2 (𝑦 = 𝐵 → (𝜓𝜒))
8 vtocl2g.3 . 2 𝜑
91, 2, 3, 4, 5, 6, 7, 8vtocl2gf 3400 1 ((𝐴𝑉𝐵𝑊) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  wcel 2131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334
This theorem is referenced by:  vtocl4g  3409  ifexg  4293  uniprg  4594  intprg  4655  opthg  5086  opelopabsb  5127  vtoclr  5313  elimasng  5641  cnvsngOLD  5774  funopg  6075  f1osng  6330  fsng  6559  fvsng  6603  fnpr2g  6630  unexb  7115  op1stg  7337  op2ndg  7338  xpsneng  8202  xpcomeng  8209  sbth  8237  unxpdom  8324  fpwwe2lem5  9640  prcdnq  9999  mhmlem  17728  carsgmon  30677  br1steqgOLD  31971  br2ndeqgOLD  31972  brimageg  32332  brdomaing  32340  brrangeg  32341  rankung  32571  mbfresfi  33761  zindbi  38005  2sbc6g  39110  2sbc5g  39111  fmulcl  40308
  Copyright terms: Public domain W3C validator