Theorem vtocl 3534

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2182. (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 236	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
5	1, 4	vtocle 3532	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844

This theorem is referenced by:  vtocl2  3540  vtoclb  3542  zfauscl  5263  fnbrfvb  6932  caovcan  7615  findcard2  9148  bnd2  9878  kmlem2  10134  axcc2lem  10419  dominf  10428  dcomex  10430  ac4c  10459  ac5  10460  dominfac  10557  grothomex  10813  ramub2  17073  ismred2  17654  utopsnneiplem  24372  dvfsumlem2  26154  plydivlem4  26425  bnj865  35255  bnj1015  35294  tz9.1regs  35469  regsfromregtco  36937  poimirlem13  38171  poimirlem14  38172  poimirlem17  38175  poimirlem20  38178  poimirlem25  38183  poimirlem28  38186  poimirlem31  38189  poimirlem32  38190  voliunnfl  38202  volsupnfl  38203  prdsbnd2  38333  iscringd  38536  monotoddzzfi  43560  monotoddzz  43561  frege104  44584  dvgrat  44913  cvgdvgrat  44914  permac8prim  45614  wessf1ornlem  45794  xrlexaddrp  45959  infleinf  45978  dvnmul  46548  dvnprodlem2  46552  fourierdlem41  46753  fourierdlem48  46759  fourierdlem49  46760  fourierdlem51  46762  fourierdlem71  46782  fourierdlem83  46794  fourierdlem97  46808  etransclem2  46841  etransclem46  46885  isomenndlem  47135  ovnsubaddlem1  47175  hoidmvlelem3  47202  vonicclem2  47289  smflimlem1  47376  smflimlem2  47377  smflimlem3  47378  funressndmafv2rn  47848