Theorem vtocl 3259

Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3260. (Contributed by NM, 30-Aug-1993.) Removed dependency on ax-10 2019. (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 3209	. . . 4 ⊢ ∃𝑥 𝑥 = 𝐴
3		vtocl.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	biimpd 219	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))
5	2, 4	eximii 1764	. . 3 ⊢ ∃𝑥(𝜑 → 𝜓)
6	5	19.36iv 1905	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
7		vtocl.3	. 2 ⊢ 𝜑
8	6, 7	mpg 1724	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990  Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  vtoclb  3263  zfauscl  4783  pwex  4848  fnbrfvb  6236  caovcan  6838  uniex  6953  findcard2  8200  zfregclOLD  8501  bnd2  8756  kmlem2  8973  axcc2lem  9258  dominf  9267  dcomex  9269  ac4c  9298  ac5  9299  dominfac  9395  pwfseqlem4  9484  grothomex  9651  ramub2  15718  ismred2  16263  utopsnneiplem  22051  dvfsumlem2  23790  plydivlem4  24051  bnj865  30993  bnj1015  31031  frmin  31739  poimirlem13  33422  poimirlem14  33423  poimirlem17  33426  poimirlem20  33429  poimirlem25  33434  poimirlem28  33437  poimirlem31  33440  poimirlem32  33441  voliunnfl  33453  volsupnfl  33454  prdsbnd2  33594  iscringd  33797  monotoddzzfi  37507  monotoddzz  37508  frege104  38261  dvgrat  38511  cvgdvgrat  38512  wessf1ornlem  39371  xrlexaddrp  39568  infleinf  39588  dvnmul  40158  dvnprodlem2  40162  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem51  40374  fourierdlem71  40394  fourierdlem83  40406  fourierdlem97  40420  etransclem2  40453  etransclem46  40497  isomenndlem  40744  ovnsubaddlem1  40784  hoidmvlelem3  40811  vonicclem2  40898  smflimlem1  40979  smflimlem2  40980  smflimlem3  40981