Theorem vtocl 3557

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  Vcvv 3479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clel 2815

This theorem is referenced by:  vtocl2  3565  vtocl3  3566  vtoclb  3567  zfauscl  5297  fnbrfvb  6958  caovcan  7638  findcard2  9205  bnd2  9934  kmlem2  10193  axcc2lem  10477  dominf  10486  dcomex  10488  ac4c  10517  ac5  10518  dominfac  10614  grothomex  10870  ramub2  17053  ismred2  17647  utopsnneiplem  24257  dvfsumlem2  26068  dvfsumlem2OLD  26069  plydivlem4  26339  bnj865  34938  bnj1015  34977  poimirlem13  37641  poimirlem14  37642  poimirlem17  37645  poimirlem20  37648  poimirlem25  37653  poimirlem28  37656  poimirlem31  37659  poimirlem32  37660  voliunnfl  37672  volsupnfl  37673  prdsbnd2  37803  iscringd  38006  monotoddzzfi  42959  monotoddzz  42960  frege104  43985  dvgrat  44336  cvgdvgrat  44337  wessf1ornlem  45195  xrlexaddrp  45368  infleinf  45388  dvnmul  45963  dvnprodlem2  45967  fourierdlem41  46168  fourierdlem48  46174  fourierdlem49  46175  fourierdlem51  46177  fourierdlem71  46197  fourierdlem83  46209  fourierdlem97  46223  etransclem2  46256  etransclem46  46300  isomenndlem  46550  ovnsubaddlem1  46590  hoidmvlelem3  46617  vonicclem2  46704  smflimlem1  46791  smflimlem2  46792  smflimlem3  46793  funressndmafv2rn  47240