Theorem vtocl 3558

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  Vcvv 3478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814

This theorem is referenced by:  vtocl2  3566  vtocl3  3567  vtoclb  3568  zfauscl  5304  fnbrfvb  6960  caovcan  7637  findcard2  9203  bnd2  9931  kmlem2  10190  axcc2lem  10474  dominf  10483  dcomex  10485  ac4c  10514  ac5  10515  dominfac  10611  grothomex  10867  ramub2  17048  ismred2  17648  utopsnneiplem  24272  dvfsumlem2  26082  dvfsumlem2OLD  26083  plydivlem4  26353  bnj865  34916  bnj1015  34955  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  42931  monotoddzz  42932  frege104  43957  dvgrat  44308  cvgdvgrat  44309  wessf1ornlem  45128  xrlexaddrp  45302  infleinf  45322  dvnmul  45899  dvnprodlem2  45903  fourierdlem41  46104  fourierdlem48  46110  fourierdlem49  46111  fourierdlem51  46113  fourierdlem71  46133  fourierdlem83  46145  fourierdlem97  46159  etransclem2  46192  etransclem46  46236  isomenndlem  46486  ovnsubaddlem1  46526  hoidmvlelem3  46553  vonicclem2  46640  smflimlem1  46727  smflimlem2  46728  smflimlem3  46729  funressndmafv2rn  47173