Theorem vtocl 3513

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

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

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 2809

This theorem is referenced by:  vtocl2  3520  vtocl3  3521  vtoclb  3522  zfauscl  5241  fnbrfvb  6882  caovcan  7560  findcard2  9087  bnd2  9803  kmlem2  10060  axcc2lem  10344  dominf  10353  dcomex  10355  ac4c  10384  ac5  10385  dominfac  10482  grothomex  10738  ramub2  16940  ismred2  17520  utopsnneiplem  24189  dvfsumlem2  25987  dvfsumlem2OLD  25988  plydivlem4  26258  bnj865  35028  bnj1015  35067  tz9.1regs  35239  poimirlem13  37773  poimirlem14  37774  poimirlem17  37777  poimirlem20  37780  poimirlem25  37785  poimirlem28  37788  poimirlem31  37791  poimirlem32  37792  voliunnfl  37804  volsupnfl  37805  prdsbnd2  37935  iscringd  38138  monotoddzzfi  43126  monotoddzz  43127  frege104  44150  dvgrat  44495  cvgdvgrat  44496  permac8prim  45197  wessf1ornlem  45371  xrlexaddrp  45539  infleinf  45558  dvnmul  46129  dvnprodlem2  46133  fourierdlem41  46334  fourierdlem48  46340  fourierdlem49  46341  fourierdlem51  46343  fourierdlem71  46363  fourierdlem83  46375  fourierdlem97  46389  etransclem2  46422  etransclem46  46466  isomenndlem  46716  ovnsubaddlem1  46756  hoidmvlelem3  46783  vonicclem2  46870  smflimlem1  46957  smflimlem2  46958  smflimlem3  46959  funressndmafv2rn  47411