Theorem riinrab

Description: Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	riinrab	⊢ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		riin0	⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = 𝐴 )
2		rzal	⊢ ( 𝑋 = ∅ → ∀ 𝑥 ∈ 𝑋 𝜑 )
3	2	ralrimivw	⊢ ( 𝑋 = ∅ → ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝑋 𝜑 )
4		rabid2	⊢ ( 𝐴 = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝑋 𝜑 )
5	3 4	sylibr	⊢ ( 𝑋 = ∅ → 𝐴 = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } )
6	1 5	eqtrd	⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } )
7		ssrab2	⊢ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
8	7	rgenw	⊢ ∀ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
9		riinn0	⊢ ( ( ∀ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
10	8 9	mpan	⊢ ( 𝑋 ≠ ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
11		iinrab	⊢ ( 𝑋 ≠ ∅ → ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } )
12	10 11	eqtrd	⊢ ( 𝑋 ≠ ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } )
13	6 12	pm2.61ine	⊢ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 }