Theorem elintrab

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999)

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

Proof

Step	Hyp	Ref	Expression
1		elintab.ex	⊢ 𝐴 ∈ V
2	1	elintab	⊢ ( 𝐴 ∈ ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) → 𝐴 ∈ 𝑥 ) )
3		impexp	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) → 𝐴 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
4	3	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) → 𝐴 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
5	2 4	bitri	⊢ ( 𝐴 ∈ ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
6		df-rab	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
7	6	inteqi	⊢ ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
8	7	eleq2i	⊢ ( 𝐴 ∈ ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝐴 ∈ ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } )
9		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝜑 → 𝐴 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
10	5 8 9	3bitr4i	⊢ ( 𝐴 ∈ ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝐵 ( 𝜑 → 𝐴 ∈ 𝑥 ) )