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

Theorem vtocl 3290
Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3291. (Contributed by NM, 30-Aug-1993.) Removed dependency on ax-10 2059. (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 3240 . . . 4 𝑥 𝑥 = 𝐴
3 vtocl.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
43biimpd 219 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
52, 4eximii 1804 . . 3 𝑥(𝜑𝜓)
6519.36iv 1914 . 2 (∀𝑥𝜑𝜓)
7 vtocl.3 . 2 𝜑
86, 7mpg 1764 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wcel 2030  Vcvv 3231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233
This theorem is referenced by:  vtoclb  3294  zfauscl  4816  pwex  4878  fnbrfvb  6274  caovcan  6880  uniex  6995  findcard2  8241  bnd2  8794  kmlem2  9011  axcc2lem  9296  dominf  9305  dcomex  9307  ac4c  9336  ac5  9337  dominfac  9433  pwfseqlem4  9522  grothomex  9689  ramub2  15765  ismred2  16310  utopsnneiplem  22098  dvfsumlem2  23835  plydivlem4  24096  bnj865  31119  bnj1015  31157  frmin  31867  poimirlem13  33552  poimirlem14  33553  poimirlem17  33556  poimirlem20  33559  poimirlem25  33564  poimirlem28  33567  poimirlem31  33570  poimirlem32  33571  voliunnfl  33583  volsupnfl  33584  prdsbnd2  33724  iscringd  33927  monotoddzzfi  37824  monotoddzz  37825  frege104  38578  dvgrat  38828  cvgdvgrat  38829  wessf1ornlem  39685  xrlexaddrp  39881  infleinf  39901  dvnmul  40476  dvnprodlem2  40480  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem51  40692  fourierdlem71  40712  fourierdlem83  40724  fourierdlem97  40738  etransclem2  40771  etransclem46  40815  isomenndlem  41065  ovnsubaddlem1  41105  hoidmvlelem3  41132  vonicclem2  41219  smflimlem1  41300  smflimlem2  41301  smflimlem3  41302
  Copyright terms: Public domain W3C validator