Theorem vtocl 3550

Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3551. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2138. (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 3490	. 2 ⊢ ∃𝑥 𝑥 = 𝐴
6	3, 5	exlimiiv 1935	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811

This theorem is referenced by:  vtocl2  3552  vtocl3  3553  vtoclb  3554  zfauscl  5302  fnbrfvb  6945  caovcan  7611  findcard2  9164  findcard2OLD  9284  bnd2  9888  kmlem2  10146  axcc2lem  10431  dominf  10440  dcomex  10442  ac4c  10471  ac5  10472  dominfac  10568  pwfseqlem4  10657  grothomex  10824  ramub2  16947  ismred2  17547  utopsnneiplem  23752  dvfsumlem2  25544  plydivlem4  25809  bnj865  33934  bnj1015  33973  gg-dvfsumlem2  35183  poimirlem13  36501  poimirlem14  36502  poimirlem17  36505  poimirlem20  36508  poimirlem25  36513  poimirlem28  36516  poimirlem31  36519  poimirlem32  36520  voliunnfl  36532  volsupnfl  36533  prdsbnd2  36663  iscringd  36866  monotoddzzfi  41681  monotoddzz  41682  frege104  42718  dvgrat  43071  cvgdvgrat  43072  wessf1ornlem  43882  xrlexaddrp  44062  infleinf  44082  dvnmul  44659  dvnprodlem2  44663  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem51  44873  fourierdlem71  44893  fourierdlem83  44905  fourierdlem97  44919  etransclem2  44952  etransclem46  44996  isomenndlem  45246  ovnsubaddlem1  45286  hoidmvlelem3  45313  vonicclem2  45400  smflimlem1  45487  smflimlem2  45488  smflimlem3  45489  funressndmafv2rn  45931