Theorem vtocl 3527

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 3524	1 ⊢ 𝜓

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

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 2804

This theorem is referenced by:  vtocl2  3535  vtocl3  3536  vtoclb  3537  zfauscl  5255  fnbrfvb  6913  caovcan  7595  findcard2  9133  bnd2  9852  kmlem2  10111  axcc2lem  10395  dominf  10404  dcomex  10406  ac4c  10435  ac5  10436  dominfac  10532  grothomex  10788  ramub2  16991  ismred2  17570  utopsnneiplem  24141  dvfsumlem2  25939  dvfsumlem2OLD  25940  plydivlem4  26210  bnj865  34919  bnj1015  34958  poimirlem13  37622  poimirlem14  37623  poimirlem17  37626  poimirlem20  37629  poimirlem25  37634  poimirlem28  37637  poimirlem31  37640  poimirlem32  37641  voliunnfl  37653  volsupnfl  37654  prdsbnd2  37784  iscringd  37987  monotoddzzfi  42924  monotoddzz  42925  frege104  43949  dvgrat  44294  cvgdvgrat  44295  permac8prim  44997  wessf1ornlem  45172  xrlexaddrp  45341  infleinf  45361  dvnmul  45934  dvnprodlem2  45938  fourierdlem41  46139  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem71  46168  fourierdlem83  46180  fourierdlem97  46194  etransclem2  46227  etransclem46  46271  isomenndlem  46521  ovnsubaddlem1  46561  hoidmvlelem3  46588  vonicclem2  46675  smflimlem1  46762  smflimlem2  46763  smflimlem3  46764  funressndmafv2rn  47214