Theorem iinrab

Description: Indexed intersection of a restricted class abstraction. (Contributed by NM, 6-Dec-2011)

	Ref	Expression
Assertion	iinrab	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		r19.28zv	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
2	1	abbidv	⊢ ( 𝐴 ≠ ∅ → { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) } )
3		df-rab	⊢ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) }
4	3	a1i	⊢ ( 𝑥 ∈ 𝐴 → { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) } )
5	4	iineq2i	⊢ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) }
6		iinab	⊢ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) }
7	5 6	eqtri	⊢ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) }
8		df-rab	⊢ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) }
9	2 7 8	3eqtr4g	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )