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

Theorem vtocl 3557
Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3558. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2136. (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 3506 . . . 4 𝑥 𝑥 = 𝐴
3 vtocl.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
43biimpd 230 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
52, 4eximii 1828 . . 3 𝑥(𝜑𝜓)
6519.36iv 1938 . 2 (∀𝑥𝜑𝜓)
7 vtocl.3 . 2 𝜑
86, 7mpg 1789 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  Vcvv 3492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890
This theorem is referenced by:  vtocl2  3559  vtocl3  3561  vtoclb  3562  zfauscl  5196  fnbrfvb  6711  caovcan  7341  uniex  7454  findcard2  8746  bnd2  9310  kmlem2  9565  axcc2lem  9846  dominf  9855  dcomex  9857  ac4c  9886  ac5  9887  dominfac  9983  pwfseqlem4  10072  grothomex  10239  ramub2  16338  ismred2  16862  utopsnneiplem  22783  dvfsumlem2  24551  plydivlem4  24812  bnj865  32094  bnj1015  32132  frmin  32981  poimirlem13  34786  poimirlem14  34787  poimirlem17  34790  poimirlem20  34793  poimirlem25  34798  poimirlem28  34801  poimirlem31  34804  poimirlem32  34805  voliunnfl  34817  volsupnfl  34818  prdsbnd2  34954  iscringd  35157  monotoddzzfi  39417  monotoddzz  39418  frege104  40191  dvgrat  40521  cvgdvgrat  40522  wessf1ornlem  41321  xrlexaddrp  41496  infleinf  41516  dvnmul  42104  dvnprodlem2  42108  fourierdlem41  42310  fourierdlem48  42316  fourierdlem49  42317  fourierdlem51  42319  fourierdlem71  42339  fourierdlem83  42351  fourierdlem97  42365  etransclem2  42398  etransclem46  42442  isomenndlem  42689  ovnsubaddlem1  42729  hoidmvlelem3  42756  vonicclem2  42843  smflimlem1  42924  smflimlem2  42925  smflimlem3  42926  funressndmafv2rn  43299
  Copyright terms: Public domain W3C validator