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

Theorem vtocl2g 3476
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2144, ax-11 2161, and ax-13 2371. (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 3416 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtocl2g.2 . . . 4 (𝑦 = 𝐵 → (𝜓𝜒))
32imbi2d 344 . . 3 (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒)))
4 vtocl2g.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
5 vtocl2g.3 . . . 4 𝜑
64, 5vtoclg 3471 . . 3 (𝐴 ∈ V → 𝜓)
73, 6vtoclg 3471 . 2 (𝐵𝑊 → (𝐴 ∈ V → 𝜒))
81, 7mpan9 510 1 ((𝐴𝑉𝐵𝑊) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wcel 2113  Vcvv 3398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400
This theorem is referenced by:  vtocl3g  3477  vtocl4g  3485  uniprgOLD  4817  intprgOLD  4873  opthg  5336  opelopabsb  5386  vtoclr  5587  elimasng  5930  funopg  6374  f1osng  6659  fsng  6910  fnpr2g  6984  unexb  7490  op1stg  7727  op2ndg  7728  xpsneng  8652  xpcomeng  8659  sbth  8688  unxpdom  8805  fpwwe2lem4  10135  prcdnq  10494  mhmlem  18338  carsgmon  31851  brimageg  33867  brdomaing  33875  brrangeg  33876  rankung  34106  mbfresfi  35443  zindbi  40332  2sbc6g  41563  2sbc5g  41564  fmulcl  42656
  Copyright terms: Public domain W3C validator