Theorem vtocl 3538

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  Vcvv 3462

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-clel 2803

This theorem is referenced by:  vtocl2  3547  vtocl3  3548  vtoclb  3549  zfauscl  5306  fnbrfvb  6954  caovcan  7630  findcard2  9202  findcard2OLD  9318  bnd2  9936  kmlem2  10194  axcc2lem  10479  dominf  10488  dcomex  10490  ac4c  10519  ac5  10520  dominfac  10616  pwfseqlem4  10705  grothomex  10872  ramub2  17016  ismred2  17616  utopsnneiplem  24243  dvfsumlem2  26052  dvfsumlem2OLD  26053  plydivlem4  26324  bnj865  34768  bnj1015  34807  poimirlem13  37334  poimirlem14  37335  poimirlem17  37338  poimirlem20  37341  poimirlem25  37346  poimirlem28  37349  poimirlem31  37352  poimirlem32  37353  voliunnfl  37365  volsupnfl  37366  prdsbnd2  37496  iscringd  37699  monotoddzzfi  42600  monotoddzz  42601  frege104  43634  dvgrat  43986  cvgdvgrat  43987  wessf1ornlem  44792  xrlexaddrp  44967  infleinf  44987  dvnmul  45564  dvnprodlem2  45568  fourierdlem41  45769  fourierdlem48  45775  fourierdlem49  45776  fourierdlem51  45778  fourierdlem71  45798  fourierdlem83  45810  fourierdlem97  45824  etransclem2  45857  etransclem46  45901  isomenndlem  46151  ovnsubaddlem1  46191  hoidmvlelem3  46218  vonicclem2  46305  smflimlem1  46392  smflimlem2  46393  smflimlem3  46394  funressndmafv2rn  46836