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

Theorem vtocl2g 3574
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2139, ax-11 2155, and ax-13 2375. (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 3499 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtocl2g.2 . . . 4 (𝑦 = 𝐵 → (𝜓𝜒))
32imbi2d 340 . . 3 (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒)))
4 vtocl2g.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
5 vtocl2g.3 . . . 4 𝜑
64, 5vtoclg 3554 . . 3 (𝐴 ∈ V → 𝜓)
73, 6vtoclg 3554 . 2 (𝐵𝑊 → (𝐴 ∈ V → 𝜒))
81, 7mpan9 506 1 ((𝐴𝑉𝐵𝑊) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  Vcvv 3478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480
This theorem is referenced by:  vtocl3g  3575  vtocl4g  3585  opthg  5488  opelopabsb  5540  vtoclr  5752  elimasngOLD  6111  funopg  6602  f1osng  6890  fsng  7157  fnpr2g  7230  unexbOLD  7767  op1stg  8025  op2ndg  8026  xpsneng  9095  xpcomeng  9103  sbth  9132  sbthfi  9237  unxpdom  9287  prcdnq  11031  mhmlem  19093  carsgmon  34296  brimageg  35909  brdomaing  35917  brrangeg  35918  rankung  36148  mbfresfi  37653  zindbi  42935  2sbc6g  44411  2sbc5g  44412  fmulcl  45537
  Copyright terms: Public domain W3C validator