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  33965  bnj1015  34004  gg-dvfsumlem2  35214  poimirlem13  36549  poimirlem14  36550  poimirlem17  36553  poimirlem20  36556  poimirlem25  36561  poimirlem28  36564  poimirlem31  36567  poimirlem32  36568  voliunnfl  36580  volsupnfl  36581  prdsbnd2  36711  iscringd  36914  monotoddzzfi  41729  monotoddzz  41730  frege104  42766  dvgrat  43119  cvgdvgrat  43120  wessf1ornlem  43930  xrlexaddrp  44110  infleinf  44130  dvnmul  44707  dvnprodlem2  44711  fourierdlem41  44912  fourierdlem48  44918  fourierdlem49  44919  fourierdlem51  44921  fourierdlem71  44941  fourierdlem83  44953  fourierdlem97  44967  etransclem2  45000  etransclem46  45044  isomenndlem  45294  ovnsubaddlem1  45334  hoidmvlelem3  45361  vonicclem2  45448  smflimlem1  45535  smflimlem2  45536  smflimlem3  45537  funressndmafv2rn  45979