Theorem vtocl 3472

Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3473. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2077. (Revised by BJ, 29-Nov-2020.)

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	. . . . 5 ⊢ 𝐴 ∈ V
2	1	isseti 3423	. . . 4 ⊢ ∃𝑥 𝑥 = 𝐴
3		vtocl.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	biimpd 221	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))
5	2, 4	eximii 1799	. . 3 ⊢ ∃𝑥(𝜑 → 𝜓)
6	5	19.36iv 1905	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
7		vtocl.3	. 2 ⊢ 𝜑
8	6, 7	mpg 1760	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ∈ wcel 2048  Vcvv 3409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-clel 2840

This theorem is referenced by:  vtocl2  3474  vtocl3  3476  vtoclb  3477  zfauscl  5056  fnbrfvb  6542  caovcan  7162  uniex  7277  findcard2  8545  bnd2  9108  kmlem2  9363  axcc2lem  9648  dominf  9657  dcomex  9659  ac4c  9688  ac5  9689  dominfac  9785  pwfseqlem4  9874  grothomex  10041  ramub2  16196  ismred2  16722  utopsnneiplem  22549  dvfsumlem2  24317  plydivlem4  24578  bnj865  31803  bnj1015  31841  frmin  32545  poimirlem13  34294  poimirlem14  34295  poimirlem17  34298  poimirlem20  34301  poimirlem25  34306  poimirlem28  34309  poimirlem31  34312  poimirlem32  34313  voliunnfl  34325  volsupnfl  34326  prdsbnd2  34463  iscringd  34666  monotoddzzfi  38880  monotoddzz  38881  frege104  39621  dvgrat  40004  cvgdvgrat  40005  wessf1ornlem  40815  xrlexaddrp  40995  infleinf  41015  dvnmul  41604  dvnprodlem2  41608  fourierdlem41  41810  fourierdlem48  41816  fourierdlem49  41817  fourierdlem51  41819  fourierdlem71  41839  fourierdlem83  41851  fourierdlem97  41865  etransclem2  41898  etransclem46  41942  isomenndlem  42189  ovnsubaddlem1  42229  hoidmvlelem3  42256  vonicclem2  42343  smflimlem1  42424  smflimlem2  42425  smflimlem3  42426  funressndmafv2rn  42774