Theorem vtocl 3519

Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3520. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2137. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.)

Hypotheses

Ref	Expression
vtocl.1	⊢ 𝐴 ∈ V
vtocl.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtocl.3	⊢ 𝜑

Assertion

Ref	Expression
vtocl	⊢ 𝜓

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtocl

Step	Hyp	Ref	Expression
1		vtocl.3	. . 3 ⊢ 𝜑
2		vtocl.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	mpbii 232	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
4		vtocl.1	. . 3 ⊢ 𝐴 ∈ V
5	4	isseti 3461	. 2 ⊢ ∃𝑥 𝑥 = 𝐴
6	3, 5	exlimiiv 1934	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  Vcvv 3446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2809

This theorem is referenced by:  vtocl2  3521  vtocl3  3522  vtoclb  3523  zfauscl  5263  fnbrfvb  6900  caovcan  7563  findcard2  9115  findcard2OLD  9235  bnd2  9838  kmlem2  10096  axcc2lem  10381  dominf  10390  dcomex  10392  ac4c  10421  ac5  10422  dominfac  10518  pwfseqlem4  10607  grothomex  10774  ramub2  16897  ismred2  17497  utopsnneiplem  23636  dvfsumlem2  25428  plydivlem4  25693  bnj865  33624  bnj1015  33663  poimirlem13  36164  poimirlem14  36165  poimirlem17  36168  poimirlem20  36171  poimirlem25  36176  poimirlem28  36179  poimirlem31  36182  poimirlem32  36183  voliunnfl  36195  volsupnfl  36196  prdsbnd2  36327  iscringd  36530  monotoddzzfi  41324  monotoddzz  41325  frege104  42361  dvgrat  42714  cvgdvgrat  42715  wessf1ornlem  43525  xrlexaddrp  43707  infleinf  43727  dvnmul  44304  dvnprodlem2  44308  fourierdlem41  44509  fourierdlem48  44515  fourierdlem49  44516  fourierdlem51  44518  fourierdlem71  44538  fourierdlem83  44550  fourierdlem97  44564  etransclem2  44597  etransclem46  44641  isomenndlem  44891  ovnsubaddlem1  44931  hoidmvlelem3  44958  vonicclem2  45045  smflimlem1  45132  smflimlem2  45133  smflimlem3  45134  funressndmafv2rn  45575