Theorem seinxp

Description: Intersection of set-like relation with Cartesian product of its field. (Contributed by Mario Carneiro, 22-Jun-2015)

	Ref	Expression
Assertion	seinxp	⊢ ( 𝑅 Se 𝐴 ↔ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) Se 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		brinxp	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
2	1	ancoms	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
3	2	rabbidva	⊢ ( 𝑥 ∈ 𝐴 → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } = { 𝑦 ∈ 𝐴 ∣ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
4	3	eleq1d	⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V ↔ { 𝑦 ∈ 𝐴 ∣ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ∈ V ) )
5	4	ralbiia	⊢ ( ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ∈ V )
6		df-se	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
7		df-se	⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ∈ V )
8	5 6 7	3bitr4i	⊢ ( 𝑅 Se 𝐴 ↔ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) Se 𝐴 )