Theorem vtocl 3562

Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3563. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2144. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.)

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.3	. . 3 ⊢ 𝜑
2		vtocl.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	mpbii 235	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
4		vtocl.1	. . 3 ⊢ 𝐴 ∈ V
5	4	isseti 3511	. 2 ⊢ ∃𝑥 𝑥 = 𝐴
6	3, 5	exlimiiv 1931	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536   ∈ wcel 2113  Vcvv 3497

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-clel 2896

This theorem is referenced by:  vtocl2  3564  vtocl3  3566  vtoclb  3567  zfauscl  5208  fnbrfvb  6721  caovcan  7355  findcard2  8761  bnd2  9325  kmlem2  9580  axcc2lem  9861  dominf  9870  dcomex  9872  ac4c  9901  ac5  9902  dominfac  9998  pwfseqlem4  10087  grothomex  10254  ramub2  16353  ismred2  16877  utopsnneiplem  22859  dvfsumlem2  24627  plydivlem4  24888  bnj865  32199  bnj1015  32238  frmin  33088  poimirlem13  34909  poimirlem14  34910  poimirlem17  34913  poimirlem20  34916  poimirlem25  34921  poimirlem28  34924  poimirlem31  34927  poimirlem32  34928  voliunnfl  34940  volsupnfl  34941  prdsbnd2  35077  iscringd  35280  monotoddzzfi  39545  monotoddzz  39546  frege104  40319  dvgrat  40650  cvgdvgrat  40651  wessf1ornlem  41451  xrlexaddrp  41626  infleinf  41646  dvnmul  42234  dvnprodlem2  42238  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem51  42449  fourierdlem71  42469  fourierdlem83  42481  fourierdlem97  42495  etransclem2  42528  etransclem46  42572  isomenndlem  42819  ovnsubaddlem1  42859  hoidmvlelem3  42886  vonicclem2  42973  smflimlem1  43054  smflimlem2  43055  smflimlem3  43056  funressndmafv2rn  43429