Theorem iinexg

Description: The existence of a class intersection. x is normally a free-variable parameter in B , which should be read B ( x ) . (Contributed by FL, 19-Sep-2011)

	Ref	Expression
Assertion	iinexg	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		dfiin2g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
2	1	adantl	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
3		elisset	⊢ ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 )
4	3	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 )
5		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) )
6	4 5	mpan2	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) )
7		r19.35	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ) )
8	6 7	sylib	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ) )
9	8	imp	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 )
10		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
11	9 10	sylib	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
12		abn0	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
13	11 12	sylibr	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ )
14		intex	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ ↔ ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )
15	13 14	sylib	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )
16	2 15	eqeltrd	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V )