Theorem elabgt

Description: Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg .) (Contributed by NM, 7-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011)

	Ref	Expression
Assertion	elabgt	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑥 𝐴
2		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
3	2	nfel2	⊢ Ⅎ 𝑥 𝐴 ∈ { 𝑥 ∣ 𝜑 }
4		nfv	⊢ Ⅎ 𝑥 𝜓
5	3 4	nfbi	⊢ Ⅎ 𝑥 ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 )
6		pm5.5	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = 𝐴 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) ) ↔ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) ) )
7	1 5 6	spcgf	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) ) )
8		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
9		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) )
10	8 9	syl5bbr	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) )
11	10	bibi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ↔ 𝜓 ) ↔ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) ) )
12	11	biimpd	⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ↔ 𝜓 ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) ) )
13	12	a2i	⊢ ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝑥 = 𝐴 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) ) )
14	13	alimi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) ) )
15	7 14	impel	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )