Theorem vtocl 3524

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2180. (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 3522	1 ⊢ 𝜓

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839

This theorem is used by:  vtocl2  3530  vtoclb  3532  zfausclOLD  5259  fnbrfvb  6966  caovcan  7657  findcard2  9218  bnd2  9993  kmlem2  10269  axcc2lem  10553  dominf  10562  dcomex  10564  ac4c  10593  ac5  10594  dominfac  10697  grothomex  10953  ramub2  17236  ismred2  17823  utopsnneiplem  24621  dvfsumlem2  26402  plydivlem4  26672  bnj865  35664  bnj1015  35703  tz9.1regs  35943  regsfromregtco  37541  poimirlem13  38819  poimirlem14  38820  poimirlem17  38823  poimirlem20  38826  poimirlem25  38831  poimirlem28  38834  poimirlem31  38837  poimirlem32  38838  voliunnfl  38850  volsupnfl  38851  prdsbnd2  38995  iscringd  39198  monotoddzzfi  44215  monotoddzz  44216  frege104  45228  dvgrat  45557  cvgdvgrat  45558  permac8prim  46268  wessf1ornlem  46473  xrlexaddrp  46637  infleinf  46656  dvnmul  47226  dvnprodlem2  47230  fourierdlem41  47431  fourierdlem48  47437  fourierdlem49  47438  fourierdlem51  47440  fourierdlem71  47460  fourierdlem83  47472  fourierdlem97  47486  etransclem2  47519  etransclem46  47563  isomenndlem  47813  ovnsubaddlem1  47853  hoidmvlelem3  47880  vonicclem2  47967  smflimlem1  48054  smflimlem2  48055  smflimlem3  48056  funressndmafv2rn  48566