Theorem vtocl 3527

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

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

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 2148

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

This theorem is used by:  vtocl2  3533  vtoclb  3535  zfausclOLD  5263  fnbrfvb  6935  caovcan  7624  findcard2  9156  bnd2  9892  kmlem2  10151  axcc2lem  10435  dominf  10444  dcomex  10446  ac4c  10475  ac5  10476  dominfac  10573  grothomex  10829  ramub2  17096  ismred2  17677  utopsnneiplem  24455  dvfsumlem2  26237  plydivlem4  26508  bnj865  35376  bnj1015  35415  tz9.1regs  35604  regsfromregtco  37106  poimirlem13  38341  poimirlem14  38342  poimirlem17  38345  poimirlem20  38348  poimirlem25  38353  poimirlem28  38356  poimirlem31  38359  poimirlem32  38360  voliunnfl  38372  volsupnfl  38373  prdsbnd2  38504  iscringd  38707  monotoddzzfi  43727  monotoddzz  43728  frege104  44751  dvgrat  45080  cvgdvgrat  45081  permac8prim  45781  wessf1ornlem  45961  xrlexaddrp  46126  infleinf  46145  dvnmul  46715  dvnprodlem2  46719  fourierdlem41  46920  fourierdlem48  46926  fourierdlem49  46927  fourierdlem51  46929  fourierdlem71  46949  fourierdlem83  46961  fourierdlem97  46975  etransclem2  47008  etransclem46  47052  isomenndlem  47302  ovnsubaddlem1  47342  hoidmvlelem3  47369  vonicclem2  47456  smflimlem1  47543  smflimlem2  47544  smflimlem3  47545  funressndmafv2rn  48018