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

Theorem vtocl 3507
 Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3508. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2142. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.)
Hypotheses
Ref Expression
vtocl.1 𝐴 ∈ V
vtocl.2 (𝑥 = 𝐴 → (𝜑𝜓))
vtocl.3 𝜑
Assertion
Ref Expression
vtocl 𝜓
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtocl
StepHypRef Expression
1 vtocl.3 . . 3 𝜑
2 vtocl.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2mpbii 236 . 2 (𝑥 = 𝐴𝜓)
4 vtocl.1 . . 3 𝐴 ∈ V
54isseti 3455 . 2 𝑥 𝑥 = 𝐴
63, 5exlimiiv 1932 1 𝜓
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  Vcvv 3441 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870 This theorem is referenced by:  vtocl2  3509  vtocl3  3511  vtoclb  3512  zfauscl  5169  fnbrfvb  6693  caovcan  7333  findcard2  8744  bnd2  9308  kmlem2  9564  axcc2lem  9849  dominf  9858  dcomex  9860  ac4c  9889  ac5  9890  dominfac  9986  pwfseqlem4  10075  grothomex  10242  ramub2  16342  ismred2  16868  utopsnneiplem  22860  dvfsumlem2  24637  plydivlem4  24899  bnj865  32317  bnj1015  32356  frmin  33209  poimirlem13  35086  poimirlem14  35087  poimirlem17  35090  poimirlem20  35093  poimirlem25  35098  poimirlem28  35101  poimirlem31  35104  poimirlem32  35105  voliunnfl  35117  volsupnfl  35118  prdsbnd2  35249  iscringd  35452  monotoddzzfi  39898  monotoddzz  39899  frege104  40683  dvgrat  41031  cvgdvgrat  41032  wessf1ornlem  41826  xrlexaddrp  41999  infleinf  42019  dvnmul  42600  dvnprodlem2  42604  fourierdlem41  42805  fourierdlem48  42811  fourierdlem49  42812  fourierdlem51  42814  fourierdlem71  42834  fourierdlem83  42846  fourierdlem97  42860  etransclem2  42893  etransclem46  42937  isomenndlem  43184  ovnsubaddlem1  43224  hoidmvlelem3  43251  vonicclem2  43338  smflimlem1  43419  smflimlem2  43420  smflimlem3  43421  funressndmafv2rn  43794
 Copyright terms: Public domain W3C validator