Theorem vtoclgf 3503

Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.)

Hypotheses

Ref	Expression
vtoclgf.1	⊢ Ⅎ𝑥𝐴
vtoclgf.2	⊢ Ⅎ𝑥𝜓
vtoclgf.3	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtoclgf.4	⊢ 𝜑

Assertion

Ref	Expression
vtoclgf	⊢ (𝐴 ∈ 𝑉 → 𝜓)

Proof of Theorem vtoclgf

Step	Hyp	Ref	Expression
1		elex 3450	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		vtoclgf.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	issetf 3446	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4		vtoclgf.2	. . . 4 ⊢ Ⅎ𝑥𝜓
5		vtoclgf.4	. . . . 5 ⊢ 𝜑
6		vtoclgf.3	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	mpbii 232	. . . 4 ⊢ (𝑥 = 𝐴 → 𝜓)
8	4, 7	exlimi 2210	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
9	3, 8	sylbi 216	. 2 ⊢ (𝐴 ∈ V → 𝜓)
10	1, 9	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wex 1782  Ⅎwnf 1786   ∈ wcel 2106  Ⅎwnfc 2887  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-v 3434

This theorem is referenced by:  vtocl2gf  3508  vtocl3gf  3509  vtoclgaf  3512  elabgf  3605  fsumsplit1  15457  ssiun2sf  30899  subtr  34503  subtr2  34504  supxrgere  42872  supxrgelem  42876  supxrge  42877  fmuldfeqlem1  43123  fprodcnlem  43140  climsuse  43149  dvnmptdivc  43479  dvmptfprodlem  43485  stoweidlem59  43600  fourierdlem31  43679  sge0f1o  43920  sge0fodjrnlem  43954