Theorem vtocl 3519

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2169. (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 235	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
5	1, 4	vtocle 3517	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1554   ∈ wcel 2136  Vcvv 3448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-clel 2831

This theorem is referenced by:  vtocl2  3526  vtoclb  3528  zfauscl  5242  fnbrfvb  6906  caovcan  7589  findcard2  9122  bnd2  9841  kmlem2  10098  axcc2lem  10383  dominf  10392  dcomex  10394  ac4c  10423  ac5  10424  dominfac  10521  grothomex  10777  ramub2  17026  ismred2  17607  utopsnneiplem  24280  dvfsumlem2  26062  plydivlem4  26330  bnj865  35175  bnj1015  35214  tz9.1regs  35385  regsfromregtco  36846  poimirlem13  38080  poimirlem14  38081  poimirlem17  38084  poimirlem20  38087  poimirlem25  38092  poimirlem28  38095  poimirlem31  38098  poimirlem32  38099  voliunnfl  38111  volsupnfl  38112  prdsbnd2  38242  iscringd  38445  monotoddzzfi  43467  monotoddzz  43468  frege104  44491  dvgrat  44836  cvgdvgrat  44837  permac8prim  45538  wessf1ornlem  45711  xrlexaddrp  45876  infleinf  45895  dvnmul  46465  dvnprodlem2  46469  fourierdlem41  46670  fourierdlem48  46676  fourierdlem49  46677  fourierdlem51  46679  fourierdlem71  46699  fourierdlem83  46711  fourierdlem97  46725  etransclem2  46758  etransclem46  46802  isomenndlem  47052  ovnsubaddlem1  47092  hoidmvlelem3  47119  vonicclem2  47206  smflimlem1  47293  smflimlem2  47294  smflimlem3  47295  funressndmafv2rn  47765