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  24111  dvfsumlem2  25909  dvfsumlem2OLD  25910  plydivlem4  26180  bnj865  34886  bnj1015  34925  poimirlem13  37600  poimirlem14  37601  poimirlem17  37604  poimirlem20  37607  poimirlem25  37612  poimirlem28  37615  poimirlem31  37618  poimirlem32  37619  voliunnfl  37631  volsupnfl  37632  prdsbnd2  37762  iscringd  37965  monotoddzzfi  42904  monotoddzz  42905  frege104  43929  dvgrat  44274  cvgdvgrat  44275  permac8prim  44977  wessf1ornlem  45152  xrlexaddrp  45321  infleinf  45341  dvnmul  45914  dvnprodlem2  45918  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  fourierdlem51  46128  fourierdlem71  46148  fourierdlem83  46160  fourierdlem97  46174  etransclem2  46207  etransclem46  46251  isomenndlem  46501  ovnsubaddlem1  46541  hoidmvlelem3  46568  vonicclem2  46655  smflimlem1  46742  smflimlem2  46743  smflimlem3  46744  funressndmafv2rn  47197