Theorem vtocl 3511

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806

This theorem is referenced by:  vtocl2  3518  vtocl3  3519  vtoclb  3520  zfauscl  5234  fnbrfvb  6872  caovcan  7550  findcard2  9074  bnd2  9786  kmlem2  10043  axcc2lem  10327  dominf  10336  dcomex  10338  ac4c  10367  ac5  10368  dominfac  10464  grothomex  10720  ramub2  16926  ismred2  17505  utopsnneiplem  24162  dvfsumlem2  25960  dvfsumlem2OLD  25961  plydivlem4  26231  bnj865  34935  bnj1015  34974  tz9.1regs  35130  poimirlem13  37681  poimirlem14  37682  poimirlem17  37685  poimirlem20  37688  poimirlem25  37693  poimirlem28  37696  poimirlem31  37699  poimirlem32  37700  voliunnfl  37712  volsupnfl  37713  prdsbnd2  37843  iscringd  38046  monotoddzzfi  42983  monotoddzz  42984  frege104  44008  dvgrat  44353  cvgdvgrat  44354  permac8prim  45055  wessf1ornlem  45230  xrlexaddrp  45399  infleinf  45418  dvnmul  45989  dvnprodlem2  45993  fourierdlem41  46194  fourierdlem48  46200  fourierdlem49  46201  fourierdlem51  46203  fourierdlem71  46223  fourierdlem83  46235  fourierdlem97  46249  etransclem2  46282  etransclem46  46326  isomenndlem  46576  ovnsubaddlem1  46616  hoidmvlelem3  46643  vonicclem2  46730  smflimlem1  46817  smflimlem2  46818  smflimlem3  46819  funressndmafv2rn  47262