Theorem vtocl 3498

Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3499. (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 3447	. 2 ⊢ ∃𝑥 𝑥 = 𝐴
6	3, 5	exlimiiv 1934	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  Vcvv 3432

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 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2816

This theorem is referenced by:  vtocl2  3500  vtocl3  3501  vtoclb  3502  zfauscl  5225  fnbrfvb  6822  caovcan  7476  findcard2  8947  findcard2OLD  9056  bnd2  9651  kmlem2  9907  axcc2lem  10192  dominf  10201  dcomex  10203  ac4c  10232  ac5  10233  dominfac  10329  pwfseqlem4  10418  grothomex  10585  ramub2  16715  ismred2  17312  utopsnneiplem  23399  dvfsumlem2  25191  plydivlem4  25456  bnj865  32903  bnj1015  32942  poimirlem13  35790  poimirlem14  35791  poimirlem17  35794  poimirlem20  35797  poimirlem25  35802  poimirlem28  35805  poimirlem31  35808  poimirlem32  35809  voliunnfl  35821  volsupnfl  35822  prdsbnd2  35953  iscringd  36156  monotoddzzfi  40764  monotoddzz  40765  frege104  41575  dvgrat  41930  cvgdvgrat  41931  wessf1ornlem  42722  xrlexaddrp  42891  infleinf  42911  dvnmul  43484  dvnprodlem2  43488  fourierdlem41  43689  fourierdlem48  43695  fourierdlem49  43696  fourierdlem51  43698  fourierdlem71  43718  fourierdlem83  43730  fourierdlem97  43744  etransclem2  43777  etransclem46  43821  isomenndlem  44068  ovnsubaddlem1  44108  hoidmvlelem3  44135  vonicclem2  44222  smflimlem1  44306  smflimlem2  44307  smflimlem3  44308  funressndmafv2rn  44715