Theorem vtocl 3524

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803

This theorem is referenced by:  vtocl2  3532  vtocl3  3533  vtoclb  3534  zfauscl  5253  fnbrfvb  6911  caovcan  7593  findcard2  9128  bnd2  9846  kmlem2  10105  axcc2lem  10389  dominf  10398  dcomex  10400  ac4c  10429  ac5  10430  dominfac  10526  grothomex  10782  ramub2  16985  ismred2  17564  utopsnneiplem  24135  dvfsumlem2  25933  dvfsumlem2OLD  25934  plydivlem4  26204  bnj865  34913  bnj1015  34952  poimirlem13  37627  poimirlem14  37628  poimirlem17  37631  poimirlem20  37634  poimirlem25  37639  poimirlem28  37642  poimirlem31  37645  poimirlem32  37646  voliunnfl  37658  volsupnfl  37659  prdsbnd2  37789  iscringd  37992  monotoddzzfi  42931  monotoddzz  42932  frege104  43956  dvgrat  44301  cvgdvgrat  44302  permac8prim  45004  wessf1ornlem  45179  xrlexaddrp  45348  infleinf  45368  dvnmul  45941  dvnprodlem2  45945  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem71  46175  fourierdlem83  46187  fourierdlem97  46201  etransclem2  46234  etransclem46  46278  isomenndlem  46528  ovnsubaddlem1  46568  hoidmvlelem3  46595  vonicclem2  46682  smflimlem1  46769  smflimlem2  46770  smflimlem3  46771  funressndmafv2rn  47221