Theorem vtocl 3488

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817

This theorem is referenced by:  vtocl2  3490  vtocl3  3491  vtoclb  3492  zfauscl  5220  fnbrfvb  6804  caovcan  7454  findcard2  8909  findcard2OLD  8986  frmin  9438  bnd2  9582  kmlem2  9838  axcc2lem  10123  dominf  10132  dcomex  10134  ac4c  10163  ac5  10164  dominfac  10260  pwfseqlem4  10349  grothomex  10516  ramub2  16643  ismred2  17229  utopsnneiplem  23307  dvfsumlem2  25096  plydivlem4  25361  bnj865  32803  bnj1015  32842  poimirlem13  35717  poimirlem14  35718  poimirlem17  35721  poimirlem20  35724  poimirlem25  35729  poimirlem28  35732  poimirlem31  35735  poimirlem32  35736  voliunnfl  35748  volsupnfl  35749  prdsbnd2  35880  iscringd  36083  monotoddzzfi  40680  monotoddzz  40681  frege104  41464  dvgrat  41819  cvgdvgrat  41820  wessf1ornlem  42611  xrlexaddrp  42781  infleinf  42801  dvnmul  43374  dvnprodlem2  43378  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem51  43588  fourierdlem71  43608  fourierdlem83  43620  fourierdlem97  43634  etransclem2  43667  etransclem46  43711  isomenndlem  43958  ovnsubaddlem1  43998  hoidmvlelem3  44025  vonicclem2  44112  smflimlem1  44193  smflimlem2  44194  smflimlem3  44195  funressndmafv2rn  44602