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

Metamath Proof Explorer

Theorem elidinxp

Description: Characterization of the elements of the intersection of the identity relation with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022)

Ref Expression
Assertion elidinxp ( 𝐶 ∈ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ )

Proof

Step Hyp Ref Expression
1 risset ⊢ ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝑥 )
2 1 anbi2ci ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝑥 ) )
3 r19.42v ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑦 = 𝑥 ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝑥 ) )
4 opeq2 ⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
5 4 equcoms ⊢ ( 𝑦 = 𝑥 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
6 5 eqeq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ↔ 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) )
7 6 pm5.32ri ⊢ ( ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑦 = 𝑥 ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 = 𝑥 ) )
8 vex ⊢ 𝑦 ∈ V
9 8 ideq ⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
10 df-br ⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
11 equcom ⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
12 9 10 11 3bitr3i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ↔ 𝑦 = 𝑥 )
13 12 anbi2i ⊢ ( ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 = 𝑥 ) )
14 7 13 bitr4i ⊢ ( ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑦 = 𝑥 ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
15 14 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑦 = 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
16 2 3 15 3bitr2i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
17 16 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
18 rexin ⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ) )
19 elinxp ⊢ ( 𝐶 ∈ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
20 17 18 19 3bitr4ri ⊢ ( 𝐶 ∈ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ )