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

Theorem vtocl2g 3577
 Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2138, ax-11 2153, and ax-13 2385. (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 3518 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtocl2g.2 . . . 4 (𝑦 = 𝐵 → (𝜓𝜒))
32imbi2d 342 . . 3 (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒)))
4 vtocl2g.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
5 vtocl2g.3 . . . 4 𝜑
64, 5vtoclg 3573 . . 3 (𝐴 ∈ V → 𝜓)
73, 6vtoclg 3573 . 2 (𝐵𝑊 → (𝐴 ∈ V → 𝜒))
81, 7mpan9 507 1 ((𝐴𝑉𝐵𝑊) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1530   ∈ wcel 2107  Vcvv 3500 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-v 3502 This theorem is referenced by:  vtocl4g  3584  uniprg  4851  intprg  4908  opthg  5366  opelopabsb  5414  vtoclr  5614  elimasng  5953  funopg  6386  f1osng  6652  fsng  6895  fnpr2g  6968  unexb  7460  op1stg  7692  op2ndg  7693  xpsneng  8591  xpcomeng  8598  sbth  8626  unxpdom  8714  fpwwe2lem5  10045  prcdnq  10404  mhmlem  18149  carsgmon  31461  brimageg  33275  brdomaing  33283  brrangeg  33284  rankung  33514  mbfresfi  34808  zindbi  39411  2sbc6g  40615  2sbc5g  40616  fmulcl  41730
 Copyright terms: Public domain W3C validator