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

Theorem vtocl 3472
Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3473. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2077. (Revised by BJ, 29-Nov-2020.)
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.1 . . . . 5 𝐴 ∈ V
21isseti 3423 . . . 4 𝑥 𝑥 = 𝐴
3 vtocl.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
43biimpd 221 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
52, 4eximii 1799 . . 3 𝑥(𝜑𝜓)
6519.36iv 1905 . 2 (∀𝑥𝜑𝜓)
7 vtocl.3 . 2 𝜑
86, 7mpg 1760 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1507  wcel 2048  Vcvv 3409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-clel 2840
This theorem is referenced by:  vtocl2  3474  vtocl3  3476  vtoclb  3477  zfauscl  5056  fnbrfvb  6542  caovcan  7162  uniex  7277  findcard2  8545  bnd2  9108  kmlem2  9363  axcc2lem  9648  dominf  9657  dcomex  9659  ac4c  9688  ac5  9689  dominfac  9785  pwfseqlem4  9874  grothomex  10041  ramub2  16196  ismred2  16722  utopsnneiplem  22549  dvfsumlem2  24317  plydivlem4  24578  bnj865  31803  bnj1015  31841  frmin  32545  poimirlem13  34294  poimirlem14  34295  poimirlem17  34298  poimirlem20  34301  poimirlem25  34306  poimirlem28  34309  poimirlem31  34312  poimirlem32  34313  voliunnfl  34325  volsupnfl  34326  prdsbnd2  34463  iscringd  34666  monotoddzzfi  38880  monotoddzz  38881  frege104  39621  dvgrat  40004  cvgdvgrat  40005  wessf1ornlem  40815  xrlexaddrp  40995  infleinf  41015  dvnmul  41604  dvnprodlem2  41608  fourierdlem41  41810  fourierdlem48  41816  fourierdlem49  41817  fourierdlem51  41819  fourierdlem71  41839  fourierdlem83  41851  fourierdlem97  41865  etransclem2  41898  etransclem46  41942  isomenndlem  42189  ovnsubaddlem1  42229  hoidmvlelem3  42256  vonicclem2  42343  smflimlem1  42424  smflimlem2  42425  smflimlem3  42426  funressndmafv2rn  42774
  Copyright terms: Public domain W3C validator