Theorem vtocl 3515

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  Vcvv 3440

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 2115

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

This theorem is referenced by:  vtocl2  3522  vtocl3  3523  vtoclb  3524  zfauscl  5243  fnbrfvb  6884  caovcan  7562  findcard2  9089  bnd2  9805  kmlem2  10062  axcc2lem  10346  dominf  10355  dcomex  10357  ac4c  10386  ac5  10387  dominfac  10484  grothomex  10740  ramub2  16942  ismred2  17522  utopsnneiplem  24191  dvfsumlem2  25989  dvfsumlem2OLD  25990  plydivlem4  26260  bnj865  35079  bnj1015  35118  tz9.1regs  35290  regsfromregtr  36668  poimirlem13  37834  poimirlem14  37835  poimirlem17  37838  poimirlem20  37841  poimirlem25  37846  poimirlem28  37849  poimirlem31  37852  poimirlem32  37853  voliunnfl  37865  volsupnfl  37866  prdsbnd2  37996  iscringd  38199  monotoddzzfi  43184  monotoddzz  43185  frege104  44208  dvgrat  44553  cvgdvgrat  44554  permac8prim  45255  wessf1ornlem  45429  xrlexaddrp  45597  infleinf  45616  dvnmul  46187  dvnprodlem2  46191  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem51  46401  fourierdlem71  46421  fourierdlem83  46433  fourierdlem97  46447  etransclem2  46480  etransclem46  46524  isomenndlem  46774  ovnsubaddlem1  46814  hoidmvlelem3  46841  vonicclem2  46928  smflimlem1  47015  smflimlem2  47016  smflimlem3  47017  funressndmafv2rn  47469