Theorem vtocl 3570

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819

This theorem is referenced by:  vtocl2  3578  vtocl3  3579  vtoclb  3580  zfauscl  5319  fnbrfvb  6973  caovcan  7654  findcard2  9230  bnd2  9962  kmlem2  10221  axcc2lem  10505  dominf  10514  dcomex  10516  ac4c  10545  ac5  10546  dominfac  10642  grothomex  10898  ramub2  17061  ismred2  17661  utopsnneiplem  24277  dvfsumlem2  26087  dvfsumlem2OLD  26088  plydivlem4  26356  bnj865  34899  bnj1015  34938  poimirlem13  37593  poimirlem14  37594  poimirlem17  37597  poimirlem20  37600  poimirlem25  37605  poimirlem28  37608  poimirlem31  37611  poimirlem32  37612  voliunnfl  37624  volsupnfl  37625  prdsbnd2  37755  iscringd  37958  monotoddzzfi  42899  monotoddzz  42900  frege104  43929  dvgrat  44281  cvgdvgrat  44282  wessf1ornlem  45092  xrlexaddrp  45267  infleinf  45287  dvnmul  45864  dvnprodlem2  45868  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem71  46098  fourierdlem83  46110  fourierdlem97  46124  etransclem2  46157  etransclem46  46201  isomenndlem  46451  ovnsubaddlem1  46491  hoidmvlelem3  46518  vonicclem2  46605  smflimlem1  46692  smflimlem2  46693  smflimlem3  46694  funressndmafv2rn  47138