Theorem vtocl 3504

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  vtocl2  3511  vtoclb  3513  zfauscl  5234  fnbrfvb  6885  caovcan  7565  findcard2  9093  bnd2  9811  kmlem2  10068  axcc2lem  10352  dominf  10361  dcomex  10363  ac4c  10392  ac5  10393  dominfac  10490  grothomex  10746  ramub2  16979  ismred2  17559  utopsnneiplem  24225  dvfsumlem2  26007  plydivlem4  26276  bnj865  35084  bnj1015  35123  tz9.1regs  35297  regsfromregtco  36739  poimirlem13  37971  poimirlem14  37972  poimirlem17  37975  poimirlem20  37978  poimirlem25  37983  poimirlem28  37986  poimirlem31  37989  poimirlem32  37990  voliunnfl  38002  volsupnfl  38003  prdsbnd2  38133  iscringd  38336  monotoddzzfi  43391  monotoddzz  43392  frege104  44415  dvgrat  44760  cvgdvgrat  44761  permac8prim  45462  wessf1ornlem  45636  xrlexaddrp  45803  infleinf  45822  dvnmul  46392  dvnprodlem2  46396  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  fourierdlem51  46606  fourierdlem71  46626  fourierdlem83  46638  fourierdlem97  46652  etransclem2  46685  etransclem46  46729  isomenndlem  46979  ovnsubaddlem1  47019  hoidmvlelem3  47046  vonicclem2  47133  smflimlem1  47220  smflimlem2  47221  smflimlem3  47222  funressndmafv2rn  47686