Theorem vtocl 3521

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

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

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  3529  vtocl3  3530  vtoclb  3531  zfauscl  5248  fnbrfvb  6893  caovcan  7573  findcard2  9105  bnd2  9822  kmlem2  10081  axcc2lem  10365  dominf  10374  dcomex  10376  ac4c  10405  ac5  10406  dominfac  10502  grothomex  10758  ramub2  16961  ismred2  17540  utopsnneiplem  24168  dvfsumlem2  25966  dvfsumlem2OLD  25967  plydivlem4  26237  bnj865  34906  bnj1015  34945  poimirlem13  37620  poimirlem14  37621  poimirlem17  37624  poimirlem20  37627  poimirlem25  37632  poimirlem28  37635  poimirlem31  37638  poimirlem32  37639  voliunnfl  37651  volsupnfl  37652  prdsbnd2  37782  iscringd  37985  monotoddzzfi  42924  monotoddzz  42925  frege104  43949  dvgrat  44294  cvgdvgrat  44295  permac8prim  44997  wessf1ornlem  45172  xrlexaddrp  45341  infleinf  45361  dvnmul  45934  dvnprodlem2  45938  fourierdlem41  46139  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem71  46168  fourierdlem83  46180  fourierdlem97  46194  etransclem2  46227  etransclem46  46271  isomenndlem  46521  ovnsubaddlem1  46561  hoidmvlelem3  46588  vonicclem2  46675  smflimlem1  46762  smflimlem2  46763  smflimlem3  46764  funressndmafv2rn  47217