Theorem vtocl 3507

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-clel 2815

This theorem is referenced by:  vtocl2  3509  vtocl3  3510  vtoclb  3511  zfauscl  5238  fnbrfvb  6859  caovcan  7514  findcard2  9004  findcard2OLD  9124  bnd2  9719  kmlem2  9977  axcc2lem  10262  dominf  10271  dcomex  10273  ac4c  10302  ac5  10303  dominfac  10399  pwfseqlem4  10488  grothomex  10655  ramub2  16782  ismred2  17379  utopsnneiplem  23470  dvfsumlem2  25262  plydivlem4  25527  bnj865  33009  bnj1015  33048  poimirlem13  35850  poimirlem14  35851  poimirlem17  35854  poimirlem20  35857  poimirlem25  35862  poimirlem28  35865  poimirlem31  35868  poimirlem32  35869  voliunnfl  35881  volsupnfl  35882  prdsbnd2  36013  iscringd  36216  monotoddzzfi  40975  monotoddzz  40976  frege104  41803  dvgrat  42158  cvgdvgrat  42159  wessf1ornlem  42957  xrlexaddrp  43134  infleinf  43154  dvnmul  43728  dvnprodlem2  43732  fourierdlem41  43933  fourierdlem48  43939  fourierdlem49  43940  fourierdlem51  43942  fourierdlem71  43962  fourierdlem83  43974  fourierdlem97  43988  etransclem2  44021  etransclem46  44065  isomenndlem  44313  ovnsubaddlem1  44353  hoidmvlelem3  44380  vonicclem2  44467  smflimlem1  44554  smflimlem2  44555  smflimlem3  44556  funressndmafv2rn  44974