Theorem vtoclgf 3392

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1620  ∃wex 1841  Ⅎwnf 1845   ∈ wcel 2127  Ⅎwnfc 2877  Vcvv 3328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330

This theorem is referenced by:  vtocl2gf  3396  vtocl3gf  3397  vtoclgaf  3399  elabgf  3476  fprodsplit1f  14891  ssiun2sf  29656  subtr  32585  subtr2  32586  supxrgere  40016  supxrgelem  40020  supxrge  40021  fsumsplit1  40276  fmuldfeqlem1  40286  fprodcnlem  40303  climsuse  40312  dvnmptdivc  40625  dvmptfprodlem  40631  stoweidlem59  40748  fourierdlem31  40827  sge0f1o  41071  sge0fodjrnlem  41105  salpreimagelt  41393  salpreimalegt  41395