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

Theorem vtocl 3254
Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3255. (Contributed by NM, 30-Aug-1993.) Removed dependency on ax-10 2017. (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 3204 . . . 4 𝑥 𝑥 = 𝐴
3 vtocl.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
43biimpd 219 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
52, 4eximii 1762 . . 3 𝑥(𝜑𝜓)
6519.36iv 1903 . 2 (∀𝑥𝜑𝜓)
7 vtocl.3 . 2 𝜑
86, 7mpg 1722 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988  Vcvv 3195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-12 2045  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1484  df-ex 1703  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-v 3197
This theorem is referenced by:  vtoclb  3258  zfauscl  4774  pwex  4839  fnbrfvb  6223  caovcan  6823  uniex  6938  findcard2  8185  zfregclOLD  8486  bnd2  8741  kmlem2  8958  axcc2lem  9243  dominf  9252  dcomex  9254  ac4c  9283  ac5  9284  dominfac  9380  pwfseqlem4  9469  grothomex  9636  ramub2  15699  ismred2  16244  utopsnneiplem  22032  dvfsumlem2  23771  plydivlem4  24032  bnj865  30967  bnj1015  31005  frmin  31713  poimirlem13  33393  poimirlem14  33394  poimirlem17  33397  poimirlem20  33400  poimirlem25  33405  poimirlem28  33408  poimirlem31  33411  poimirlem32  33412  voliunnfl  33424  volsupnfl  33425  prdsbnd2  33565  iscringd  33768  monotoddzzfi  37326  monotoddzz  37327  frege104  38081  dvgrat  38331  cvgdvgrat  38332  wessf1ornlem  39187  xrlexaddrp  39381  infleinf  39401  dvnmul  39921  dvnprodlem2  39925  fourierdlem41  40128  fourierdlem48  40134  fourierdlem49  40135  fourierdlem51  40137  fourierdlem71  40157  fourierdlem83  40169  fourierdlem97  40183  etransclem2  40216  etransclem46  40260  isomenndlem  40507  ovnsubaddlem1  40547  hoidmvlelem3  40574  vonicclem2  40661  smflimlem1  40742  smflimlem2  40743  smflimlem3  40744
  Copyright terms: Public domain W3C validator