Theorem vtoclgf 3464

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601  ∃wex 1823  Ⅎwnf 1827   ∈ wcel 2106  Ⅎwnfc 2918  Vcvv 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399

This theorem is referenced by:  vtocl2gf  3468  vtocl3gf  3469  vtoclgaf  3472  elabgf  3553  ssiun2sf  29940  subtr  32897  subtr2  32898  supxrgere  40439  supxrgelem  40443  supxrge  40444  fsumsplit1  40694  fmuldfeqlem1  40704  fprodcnlem  40721  climsuse  40730  dvnmptdivc  41063  dvmptfprodlem  41069  stoweidlem59  41185  fourierdlem31  41264  sge0f1o  41505  sge0fodjrnlem  41539  salpreimagelt  41827  salpreimalegt  41829