Theorem vtoclgf 3126

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

Syntax hints:   → wi 4   ↔ wb 191   = wceq 1468  ∃wex 1692  Ⅎwnf 1696   ∈ wcel 1937  Ⅎwnfc 2633  Vcvv 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485

This theorem depends on definitions:  df-bi 192  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-v 3068

This theorem is referenced by:  vtocl2gf  3130  vtocl3gf  3131  vtoclgaf  3133  elabgf  3206  fprodsplit1f  14204  ssiun2sf  28334  subtr  31119  subtr2  31120  supxrgere  37932  supxrgelem  37936  supxrge  37937  fsumsplit1  38052  fmuldfeqlem1  38062  fprodcnlem  38081  climsuse  38091  dvnmptdivc  38232  dvmptfprodlem  38238  stoweidlem59  38356  fourierdlem31  38436  fourierdlem31OLD  38437  sge0f1o  38670  sge0fodjrnlem  38704