Theorem vtocl 3232

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  vtoclb  3236  zfauscl  4711  pwex  4774  fnbrfvb  6146  caovcan  6736  uniex  6851  findcard2  8085  zfregclOLD  8384  bnd2  8639  kmlem2  8856  axcc2lem  9141  dominf  9150  dcomex  9152  ac4c  9181  ac5  9182  dominfac  9274  pwfseqlem4  9363  grothomex  9530  ramub2  15556  ismred2  16086  utopsnneiplem  21861  dvfsumlem2  23594  plydivlem4  23855  bnj865  30247  bnj1015  30285  frmin  30983  poimirlem13  32592  poimirlem14  32593  poimirlem17  32596  poimirlem20  32599  poimirlem25  32604  poimirlem28  32607  poimirlem31  32610  poimirlem32  32611  voliunnfl  32623  volsupnfl  32624  prdsbnd2  32764  iscringd  32967  monotoddzzfi  36525  monotoddzz  36526  frege104  37281  dvgrat  37533  cvgdvgrat  37534  wessf1ornlem  38366  xrlexaddrp  38509  infleinf  38529  dvnmul  38833  dvnprodlem2  38837  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem71  39070  fourierdlem83  39082  fourierdlem97  39096  etransclem2  39129  etransclem46  39173  isomenndlem  39420  ovnsubaddlem1  39460  hoidmvlelem3  39487  vonicclem2  39575  smflimlem1  39657  smflimlem2  39658  smflimlem3  39659