Theorem vtocl 3542

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2810

This theorem is referenced by:  vtocl2  3550  vtocl3  3551  vtoclb  3552  zfauscl  5273  fnbrfvb  6934  caovcan  7616  findcard2  9183  bnd2  9912  kmlem2  10171  axcc2lem  10455  dominf  10464  dcomex  10466  ac4c  10495  ac5  10496  dominfac  10592  grothomex  10848  ramub2  17039  ismred2  17620  utopsnneiplem  24191  dvfsumlem2  25990  dvfsumlem2OLD  25991  plydivlem4  26261  bnj865  34959  bnj1015  34998  poimirlem13  37662  poimirlem14  37663  poimirlem17  37666  poimirlem20  37669  poimirlem25  37674  poimirlem28  37677  poimirlem31  37680  poimirlem32  37681  voliunnfl  37693  volsupnfl  37694  prdsbnd2  37824  iscringd  38027  monotoddzzfi  42933  monotoddzz  42934  frege104  43958  dvgrat  44303  cvgdvgrat  44304  wessf1ornlem  45176  xrlexaddrp  45346  infleinf  45366  dvnmul  45939  dvnprodlem2  45943  fourierdlem41  46144  fourierdlem48  46150  fourierdlem49  46151  fourierdlem51  46153  fourierdlem71  46173  fourierdlem83  46185  fourierdlem97  46199  etransclem2  46232  etransclem46  46276  isomenndlem  46526  ovnsubaddlem1  46566  hoidmvlelem3  46593  vonicclem2  46680  smflimlem1  46767  smflimlem2  46768  smflimlem3  46769  funressndmafv2rn  47219