Theorem vtocl 3517

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

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

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  3524  vtocl3  3525  vtoclb  3526  zfauscl  5245  fnbrfvb  6892  caovcan  7572  findcard2  9101  bnd2  9817  kmlem2  10074  axcc2lem  10358  dominf  10367  dcomex  10369  ac4c  10398  ac5  10399  dominfac  10496  grothomex  10752  ramub2  16954  ismred2  17534  utopsnneiplem  24203  dvfsumlem2  26001  dvfsumlem2OLD  26002  plydivlem4  26272  bnj865  35099  bnj1015  35138  tz9.1regs  35312  regsfromregtr  36690  poimirlem13  37884  poimirlem14  37885  poimirlem17  37888  poimirlem20  37891  poimirlem25  37896  poimirlem28  37899  poimirlem31  37902  poimirlem32  37903  voliunnfl  37915  volsupnfl  37916  prdsbnd2  38046  iscringd  38249  monotoddzzfi  43299  monotoddzz  43300  frege104  44323  dvgrat  44668  cvgdvgrat  44669  permac8prim  45370  wessf1ornlem  45544  xrlexaddrp  45711  infleinf  45730  dvnmul  46301  dvnprodlem2  46305  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  fourierdlem51  46515  fourierdlem71  46535  fourierdlem83  46547  fourierdlem97  46561  etransclem2  46594  etransclem46  46638  isomenndlem  46888  ovnsubaddlem1  46928  hoidmvlelem3  46955  vonicclem2  47042  smflimlem1  47129  smflimlem2  47130  smflimlem3  47131  funressndmafv2rn  47583