This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 )