Theorem vtocl 3520

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2178. (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 1570   ∈ wcel 2145  Vcvv 3450

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 1943  ax-6 2000  ax-7 2041  ax-8 2147

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

This theorem is used by:  vtocl2  3526  vtoclb  3528  zfausclOLD  5255  fnbrfvb  6928  caovcan  7618  findcard2  9159  bnd2  9895  kmlem2  10154  axcc2lem  10438  dominf  10447  dcomex  10449  ac4c  10478  ac5  10479  dominfac  10582  grothomex  10838  ramub2  17106  ismred2  17687  utopsnneiplem  24473  dvfsumlem2  26254  plydivlem4  26526  bnj865  35432  bnj1015  35471  tz9.1regs  35660  regsfromregtco  37157  poimirlem13  38382  poimirlem14  38383  poimirlem17  38386  poimirlem20  38389  poimirlem25  38394  poimirlem28  38397  poimirlem31  38400  poimirlem32  38401  voliunnfl  38413  volsupnfl  38414  prdsbnd2  38545  iscringd  38748  monotoddzzfi  43783  monotoddzz  43784  frege104  44807  dvgrat  45136  cvgdvgrat  45137  permac8prim  45837  wessf1ornlem  46017  xrlexaddrp  46182  infleinf  46201  dvnmul  46771  dvnprodlem2  46775  fourierdlem41  46976  fourierdlem48  46982  fourierdlem49  46983  fourierdlem51  46985  fourierdlem71  47005  fourierdlem83  47017  fourierdlem97  47031  etransclem2  47064  etransclem46  47108  isomenndlem  47358  ovnsubaddlem1  47398  hoidmvlelem3  47425  vonicclem2  47512  smflimlem1  47599  smflimlem2  47600  smflimlem3  47601  funressndmafv2rn  48111