Theorem vtocl 3525

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2176. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.) (Proof shortened by Wolf Lammen, 20-Jun-2025.)

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.1	. 2 ⊢ 𝐴 ∈ V
2		vtocl.3	. . 3 ⊢ 𝜑
3		vtocl.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	2, 3	mpbii 236	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
5	1, 4	vtocle 3523	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838

This theorem is referenced by:  vtocl2  3531  vtoclb  3533  zfausclOLD  5261  fnbrfvb  6931  caovcan  7614  findcard2  9145  bnd2  9875  kmlem2  10131  axcc2lem  10415  dominf  10424  dcomex  10426  ac4c  10455  ac5  10456  dominfac  10553  grothomex  10809  ramub2  17069  ismred2  17650  utopsnneiplem  24404  dvfsumlem2  26186  plydivlem4  26457  bnj865  35311  bnj1015  35350  tz9.1regs  35547  regsfromregtco  37049  poimirlem13  38284  poimirlem14  38285  poimirlem17  38288  poimirlem20  38291  poimirlem25  38296  poimirlem28  38299  poimirlem31  38302  poimirlem32  38303  voliunnfl  38315  volsupnfl  38316  prdsbnd2  38446  iscringd  38649  monotoddzzfi  43669  monotoddzz  43670  frege104  44693  dvgrat  45022  cvgdvgrat  45023  permac8prim  45723  wessf1ornlem  45903  xrlexaddrp  46068  infleinf  46087  dvnmul  46657  dvnprodlem2  46661  fourierdlem41  46862  fourierdlem48  46868  fourierdlem49  46869  fourierdlem51  46871  fourierdlem71  46891  fourierdlem83  46903  fourierdlem97  46917  etransclem2  46950  etransclem46  46994  isomenndlem  47244  ovnsubaddlem1  47284  hoidmvlelem3  47311  vonicclem2  47398  smflimlem1  47485  smflimlem2  47486  smflimlem3  47487  funressndmafv2rn  47960