Theorem vtocl 3520

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835

This theorem is used by:  vtocl2  3526  vtoclb  3528  zfausclOLD  5252  fnbrfvb  6940  caovcan  7629  findcard2  9187  bnd2  9963  kmlem2  10237  axcc2lem  10521  dominf  10530  dcomex  10532  ac4c  10561  ac5  10562  dominfac  10665  grothomex  10921  ramub2  17201  ismred2  17782  utopsnneiplem  24575  dvfsumlem2  26356  plydivlem4  26626  bnj865  35603  bnj1015  35642  tz9.1regs  35862  regsfromregtco  37422  poimirlem13  38660  poimirlem14  38661  poimirlem17  38664  poimirlem20  38667  poimirlem25  38672  poimirlem28  38675  poimirlem31  38678  poimirlem32  38679  voliunnfl  38691  volsupnfl  38692  prdsbnd2  38838  iscringd  39041  monotoddzzfi  44058  monotoddzz  44059  frege104  45076  dvgrat  45405  cvgdvgrat  45406  permac8prim  46112  wessf1ornlem  46308  xrlexaddrp  46472  infleinf  46491  dvnmul  47061  dvnprodlem2  47065  fourierdlem41  47266  fourierdlem48  47272  fourierdlem49  47273  fourierdlem51  47275  fourierdlem71  47295  fourierdlem83  47307  fourierdlem97  47321  etransclem2  47354  etransclem46  47398  isomenndlem  47648  ovnsubaddlem1  47688  hoidmvlelem3  47715  vonicclem2  47802  smflimlem1  47889  smflimlem2  47890  smflimlem3  47891  funressndmafv2rn  48401