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

Theorem vtocl 3231
Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3232. (Contributed by NM, 30-Aug-1993.) Removed dependency on ax-10 2005. (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 3181 . . . 4 𝑥 𝑥 = 𝐴
3 vtocl.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
43biimpd 217 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
52, 4eximii 1753 . . 3 𝑥(𝜑𝜓)
6519.36iv 1891 . 2 (∀𝑥𝜑𝜓)
7 vtocl.3 . 2 𝜑
86, 7mpg 1714 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  Vcvv 3172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2032  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-v 3174
This theorem is referenced by:  vtoclb  3235  zfauscl  4705  pwex  4769  fnbrfvb  6131  caovcan  6713  uniex  6828  findcard2  8062  zfregclOLD  8361  bnd2  8616  kmlem2  8833  axcc2lem  9118  dominf  9127  dcomex  9129  ac4c  9158  ac5  9159  dominfac  9251  pwfseqlem4  9340  grothomex  9507  ramub2  15502  ismred2  16032  utopsnneiplem  21803  dvfsumlem2  23511  plydivlem4  23772  bnj865  30053  bnj1015  30091  frmin  30789  poimirlem13  32395  poimirlem14  32396  poimirlem17  32399  poimirlem20  32402  poimirlem25  32407  poimirlem28  32410  poimirlem31  32413  poimirlem32  32414  voliunnfl  32426  volsupnfl  32427  prdsbnd2  32567  iscringd  32770  monotoddzzfi  36328  monotoddzz  36329  frege104  37084  dvgrat  37336  cvgdvgrat  37337  wessf1ornlem  38169  xrlexaddrp  38313  infleinf  38333  dvnmul  38637  dvnprodlem2  38641  fourierdlem41  38845  fourierdlem48  38851  fourierdlem49  38852  fourierdlem51  38854  fourierdlem71  38874  fourierdlem83  38886  fourierdlem97  38900  etransclem2  38933  etransclem46  38977  isomenndlem  39224  ovnsubaddlem1  39264  hoidmvlelem3  39291  vonicclem2  39379  smflimlem1  39461  smflimlem2  39462  smflimlem3  39463
  Copyright terms: Public domain W3C validator