Theorem vtocl 3525

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2175. (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 235	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
5	1, 4	vtocle 3523	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   ∈ wcel 2142  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-clel 2837

This theorem is referenced by:  vtocl2  3531  vtoclb  3533  zfauscl  5248  fnbrfvb  6917  caovcan  7600  findcard2  9133  bnd2  9851  kmlem2  10108  axcc2lem  10393  dominf  10402  dcomex  10404  ac4c  10433  ac5  10434  dominfac  10531  grothomex  10787  ramub2  17050  ismred2  17631  utopsnneiplem  24304  dvfsumlem2  26086  plydivlem4  26357  bnj865  35215  bnj1015  35254  tz9.1regs  35427  regsfromregtco  36895  poimirlem13  38129  poimirlem14  38130  poimirlem17  38133  poimirlem20  38136  poimirlem25  38141  poimirlem28  38144  poimirlem31  38147  poimirlem32  38148  voliunnfl  38160  volsupnfl  38161  prdsbnd2  38291  iscringd  38494  monotoddzzfi  43516  monotoddzz  43517  frege104  44540  dvgrat  44885  cvgdvgrat  44886  permac8prim  45587  wessf1ornlem  45760  xrlexaddrp  45925  infleinf  45944  dvnmul  46514  dvnprodlem2  46518  fourierdlem41  46719  fourierdlem48  46725  fourierdlem49  46726  fourierdlem51  46728  fourierdlem71  46748  fourierdlem83  46760  fourierdlem97  46774  etransclem2  46807  etransclem46  46851  isomenndlem  47101  ovnsubaddlem1  47141  hoidmvlelem3  47168  vonicclem2  47255  smflimlem1  47342  smflimlem2  47343  smflimlem3  47344  funressndmafv2rn  47814