Theorem vtocl 3513

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

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

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  3521  vtocl3  3522  vtoclb  3523  zfauscl  5237  fnbrfvb  6873  caovcan  7553  findcard2  9078  bnd2  9789  kmlem2  10046  axcc2lem  10330  dominf  10339  dcomex  10341  ac4c  10370  ac5  10371  dominfac  10467  grothomex  10723  ramub2  16926  ismred2  17505  utopsnneiplem  24133  dvfsumlem2  25931  dvfsumlem2OLD  25932  plydivlem4  26202  bnj865  34890  bnj1015  34929  tz9.1regs  35067  poimirlem13  37613  poimirlem14  37614  poimirlem17  37617  poimirlem20  37620  poimirlem25  37625  poimirlem28  37628  poimirlem31  37631  poimirlem32  37632  voliunnfl  37644  volsupnfl  37645  prdsbnd2  37775  iscringd  37978  monotoddzzfi  42915  monotoddzz  42916  frege104  43940  dvgrat  44285  cvgdvgrat  44286  permac8prim  44988  wessf1ornlem  45163  xrlexaddrp  45332  infleinf  45351  dvnmul  45924  dvnprodlem2  45928  fourierdlem41  46129  fourierdlem48  46135  fourierdlem49  46136  fourierdlem51  46138  fourierdlem71  46158  fourierdlem83  46170  fourierdlem97  46184  etransclem2  46217  etransclem46  46261  isomenndlem  46511  ovnsubaddlem1  46551  hoidmvlelem3  46578  vonicclem2  46665  smflimlem1  46752  smflimlem2  46753  smflimlem3  46754  funressndmafv2rn  47207