Theorem vtocl 3521

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 3519	1 ⊢ 𝜓

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

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 2836

This theorem is used by:  vtocl2  3527  vtoclb  3529  zfausclOLD  5253  fnbrfvb  6933  caovcan  7623  findcard2  9173  bnd2  9949  kmlem2  10223  axcc2lem  10507  dominf  10516  dcomex  10518  ac4c  10547  ac5  10548  dominfac  10651  grothomex  10907  ramub2  17185  ismred2  17766  utopsnneiplem  24559  dvfsumlem2  26340  plydivlem4  26610  bnj865  35546  bnj1015  35585  tz9.1regs  35785  regsfromregtco  37306  poimirlem13  38531  poimirlem14  38532  poimirlem17  38535  poimirlem20  38538  poimirlem25  38543  poimirlem28  38546  poimirlem31  38549  poimirlem32  38550  voliunnfl  38562  volsupnfl  38563  prdsbnd2  38709  iscringd  38912  monotoddzzfi  43928  monotoddzz  43929  frege104  44952  dvgrat  45281  cvgdvgrat  45282  permac8prim  45982  wessf1ornlem  46169  xrlexaddrp  46333  infleinf  46352  dvnmul  46922  dvnprodlem2  46926  fourierdlem41  47127  fourierdlem48  47133  fourierdlem49  47134  fourierdlem51  47136  fourierdlem71  47156  fourierdlem83  47168  fourierdlem97  47182  etransclem2  47215  etransclem46  47259  isomenndlem  47509  ovnsubaddlem1  47549  hoidmvlelem3  47576  vonicclem2  47663  smflimlem1  47750  smflimlem2  47751  smflimlem3  47752  funressndmafv2rn  48262