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

Theorem vtocl2g 3562
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 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 3492 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtocl2g.2 . . . 4 (𝑦 = 𝐵 → (𝜓𝜒))
32imbi2d 340 . . 3 (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒)))
4 vtocl2g.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
5 vtocl2g.3 . . . 4 𝜑
64, 5vtoclg 3556 . . 3 (𝐴 ∈ V → 𝜓)
73, 6vtoclg 3556 . 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 3474
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 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476
This theorem is referenced by:  vtocl3g  3563  vtocl4g  3571  uniprgOLD  4928  intprgOLD  4988  opthg  5477  opelopabsb  5530  vtoclr  5739  elimasngOLD  6089  funopg  6582  f1osng  6874  fsng  7137  fnpr2g  7214  unexb  7737  op1stg  7989  op2ndg  7990  xpsneng  9058  xpcomeng  9066  sbth  9095  sbthfi  9204  unxpdom  9255  fpwwe2lem4  10631  prcdnq  10990  mhmlem  18981  carsgmon  33599  brimageg  35191  brdomaing  35199  brrangeg  35200  rankung  35430  mbfresfi  36837  zindbi  41987  2sbc6g  43476  2sbc5g  43477  fmulcl  44596
  Copyright terms: Public domain W3C validator