Theorem vtoclgf 3514

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 3454	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		vtoclgf.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	issetf 3450	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4		vtoclgf.2	. . . 4 ⊢ Ⅎ𝑥𝜓
5		vtoclgf.4	. . . . 5 ⊢ 𝜑
6		vtoclgf.3	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	mpbii 235	. . . 4 ⊢ (𝑥 = 𝐴 → 𝜓)
8	4, 7	exlimi 2231	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → 𝜓)
9	3, 8	sylbi 219	. 2 ⊢ (𝐴 ∈ V → 𝜓)
10	1, 9	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  ∃wex 1787  Ⅎwnf 1791   ∈ wcel 2121  Ⅎwnfc 2888  Vcvv 3433

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 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-v 3435

This theorem is referenced by:  vtocl2gf  3516  vtocl3gf  3517  vtoclgaf  3520  elabgf  3613  fsumsplit1  15702  ssiun2sf  32650  subtr  36555  subtr2  36556  supxrgere  45790  supxrgelem  45794  supxrge  45795  fmuldfeqlem1  46039  climsuse  46065  dvnmptdivc  46393  dvmptfprodlem  46399  stoweidlem59  46514  fourierdlem31  46593  sge0fodjrnlem  46871