Theorem elintab

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993)

	Ref	Expression
Hypothesis	inteqab.1	⊢ 𝐴 ∈ V
Assertion	elintab	⊢ ( 𝐴 ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		inteqab.1	⊢ 𝐴 ∈ V
2	1	elint	⊢ ( 𝐴 ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝐴 ∈ 𝑦 ) )
3		nfsab1	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 }
4		nfv	⊢ Ⅎ 𝑥 𝐴 ∈ 𝑦
5	3 4	nfim	⊢ Ⅎ 𝑥 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝐴 ∈ 𝑦 )
6		nfv	⊢ Ⅎ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 )
7		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑥 ∣ 𝜑 } ) )
8		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
9	7 8	bitrdi	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 ) )
10		eleq2w	⊢ ( 𝑦 = 𝑥 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥 ) )
11	9 10	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝐴 ∈ 𝑦 ) ↔ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
12	5 6 11	cbvalv1	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝐴 ∈ 𝑦 ) ↔ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) )
13	2 12	bitri	⊢ ( 𝐴 ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) )