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

Theorem vtocl2g 3563
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2138, ax-11 2155, and ax-13 2372. (Revised by Steven Nguyen, 29-Nov-2022.)
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 elex 3493 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtocl2g.2 . . . 4 (𝑦 = 𝐵 → (𝜓𝜒))
32imbi2d 341 . . 3 (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒)))
4 vtocl2g.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
5 vtocl2g.3 . . . 4 𝜑
64, 5vtoclg 3557 . . 3 (𝐴 ∈ V → 𝜓)
73, 6vtoclg 3557 . 2 (𝐵𝑊 → (𝐴 ∈ V → 𝜒))
81, 7mpan9 508 1 ((𝐴𝑉𝐵𝑊) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  Vcvv 3475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477
This theorem is referenced by:  vtocl3g  3564  vtocl4g  3572  uniprgOLD  4929  intprgOLD  4989  opthg  5478  opelopabsb  5531  vtoclr  5740  elimasngOLD  6090  funopg  6583  f1osng  6875  fsng  7135  fnpr2g  7212  unexb  7735  op1stg  7987  op2ndg  7988  xpsneng  9056  xpcomeng  9064  sbth  9093  sbthfi  9202  unxpdom  9253  fpwwe2lem4  10629  prcdnq  10988  mhmlem  18945  carsgmon  33344  brimageg  34930  brdomaing  34938  brrangeg  34939  rankung  35169  mbfresfi  36582  zindbi  41733  2sbc6g  43222  2sbc5g  43223  fmulcl  44345
  Copyright terms: Public domain W3C validator