Theorem vtocl 3474

Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3475. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2141. (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 236	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
4		vtocl.1	. . 3 ⊢ 𝐴 ∈ V
5	4	isseti 3423	. 2 ⊢ ∃𝑥 𝑥 = 𝐴
6	3, 5	exlimiiv 1939	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2110  Vcvv 3408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-clel 2816

This theorem is referenced by:  vtocl2  3476  vtocl3  3477  vtoclb  3478  zfauscl  5194  fnbrfvb  6765  caovcan  7412  findcard2  8842  findcard2OLD  8913  frmin  9365  bnd2  9509  kmlem2  9765  axcc2lem  10050  dominf  10059  dcomex  10061  ac4c  10090  ac5  10091  dominfac  10187  pwfseqlem4  10276  grothomex  10443  ramub2  16567  ismred2  17106  utopsnneiplem  23145  dvfsumlem2  24924  plydivlem4  25189  bnj865  32616  bnj1015  32655  poimirlem13  35527  poimirlem14  35528  poimirlem17  35531  poimirlem20  35534  poimirlem25  35539  poimirlem28  35542  poimirlem31  35545  poimirlem32  35546  voliunnfl  35558  volsupnfl  35559  prdsbnd2  35690  iscringd  35893  monotoddzzfi  40467  monotoddzz  40468  frege104  41252  dvgrat  41603  cvgdvgrat  41604  wessf1ornlem  42395  xrlexaddrp  42564  infleinf  42584  dvnmul  43159  dvnprodlem2  43163  fourierdlem41  43364  fourierdlem48  43370  fourierdlem49  43371  fourierdlem51  43373  fourierdlem71  43393  fourierdlem83  43405  fourierdlem97  43419  etransclem2  43452  etransclem46  43496  isomenndlem  43743  ovnsubaddlem1  43783  hoidmvlelem3  43810  vonicclem2  43897  smflimlem1  43978  smflimlem2  43979  smflimlem3  43980  funressndmafv2rn  44387