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

Theorem vtocl2g 3559
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2137, ax-11 2154, and ax-13 2370. (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 3491 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtocl2g.2 . . . 4 (𝑦 = 𝐵 → (𝜓𝜒))
32imbi2d 340 . . 3 (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒)))
4 vtocl2g.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
5 vtocl2g.3 . . . 4 𝜑
64, 5vtoclg 3553 . . 3 (𝐴 ∈ V → 𝜓)
73, 6vtoclg 3553 . 2 (𝐵𝑊 → (𝐴 ∈ V → 𝜒))
81, 7mpan9 507 1 ((𝐴𝑉𝐵𝑊) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  Vcvv 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475
This theorem is referenced by:  vtocl3g  3560  vtocl4g  3568  uniprgOLD  4921  intprgOLD  4981  opthg  5470  opelopabsb  5523  vtoclr  5731  elimasngOLD  6078  funopg  6571  f1osng  6861  fsng  7119  fnpr2g  7196  unexb  7718  op1stg  7969  op2ndg  7970  xpsneng  9039  xpcomeng  9047  sbth  9076  sbthfi  9185  unxpdom  9236  fpwwe2lem4  10611  prcdnq  10970  mhmlem  18917  carsgmon  33144  brimageg  34729  brdomaing  34737  brrangeg  34738  rankung  34968  mbfresfi  36338  zindbi  41456  2sbc6g  42945  2sbc5g  42946  fmulcl  44070
  Copyright terms: Public domain W3C validator