Theorem vtocl 3503

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

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

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 2811

This theorem is referenced by:  vtocl2  3510  vtoclb  3512  zfauscl  5233  fnbrfvb  6890  caovcan  7571  findcard2  9099  bnd2  9817  kmlem2  10074  axcc2lem  10358  dominf  10367  dcomex  10369  ac4c  10398  ac5  10399  dominfac  10496  grothomex  10752  ramub2  16985  ismred2  17565  utopsnneiplem  24212  dvfsumlem2  25994  plydivlem4  26262  bnj865  35065  bnj1015  35104  tz9.1regs  35278  regsfromregtco  36720  poimirlem13  37954  poimirlem14  37955  poimirlem17  37958  poimirlem20  37961  poimirlem25  37966  poimirlem28  37969  poimirlem31  37972  poimirlem32  37973  voliunnfl  37985  volsupnfl  37986  prdsbnd2  38116  iscringd  38319  monotoddzzfi  43370  monotoddzz  43371  frege104  44394  dvgrat  44739  cvgdvgrat  44740  permac8prim  45441  wessf1ornlem  45615  xrlexaddrp  45782  infleinf  45801  dvnmul  46371  dvnprodlem2  46375  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem71  46605  fourierdlem83  46617  fourierdlem97  46631  etransclem2  46664  etransclem46  46708  isomenndlem  46958  ovnsubaddlem1  46998  hoidmvlelem3  47025  vonicclem2  47112  smflimlem1  47199  smflimlem2  47200  smflimlem3  47201  funressndmafv2rn  47671