Theorem vtocl 3503

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814

This theorem is referenced by:  vtocl2  3510  vtoclb  3512  zfauscl  5220  fnbrfvb  6877  caovcan  7560  findcard2  9089  bnd2  9808  kmlem2  10065  axcc2lem  10349  dominf  10358  dcomex  10360  ac4c  10389  ac5  10390  dominfac  10487  grothomex  10743  ramub2  16976  ismred2  17556  utopsnneiplem  24230  dvfsumlem2  26012  plydivlem4  26280  bnj865  35105  bnj1015  35144  tz9.1regs  35315  regsfromregtco  36766  poimirlem13  38000  poimirlem14  38001  poimirlem17  38004  poimirlem20  38007  poimirlem25  38012  poimirlem28  38015  poimirlem31  38018  poimirlem32  38019  voliunnfl  38031  volsupnfl  38032  prdsbnd2  38162  iscringd  38365  monotoddzzfi  43387  monotoddzz  43388  frege104  44411  dvgrat  44756  cvgdvgrat  44757  permac8prim  45458  wessf1ornlem  45632  xrlexaddrp  45797  infleinf  45816  dvnmul  46386  dvnprodlem2  46390  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  fourierdlem51  46600  fourierdlem71  46620  fourierdlem83  46632  fourierdlem97  46646  etransclem2  46679  etransclem46  46723  isomenndlem  46973  ovnsubaddlem1  47013  hoidmvlelem3  47040  vonicclem2  47127  smflimlem1  47214  smflimlem2  47215  smflimlem3  47216  funressndmafv2rn  47686