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

Metamath Proof Explorer

Theorem eqrelf

Description: The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019)

Ref Expression
Hypotheses eqrelf.1 ⊢ Ⅎ 𝑥 𝐴
eqrelf.2 ⊢ Ⅎ 𝑥 𝐵
eqrelf.3 ⊢ Ⅎ 𝑦 𝐴
eqrelf.4 ⊢ Ⅎ 𝑦 𝐵
Assertion eqrelf ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eqrelf.1 ⊢ Ⅎ 𝑥 𝐴
2 eqrelf.2 ⊢ Ⅎ 𝑥 𝐵
3 eqrelf.3 ⊢ Ⅎ 𝑦 𝐴
4 eqrelf.4 ⊢ Ⅎ 𝑦 𝐵
5 eqrel ⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑢 ∀ 𝑣 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ) ) )
6 nfv ⊢ Ⅎ 𝑢 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
7 nfv ⊢ Ⅎ 𝑣 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
8 1 nfel2 ⊢ Ⅎ 𝑥 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴
9 2 nfel2 ⊢ Ⅎ 𝑥 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵
10 8 9 nfbi ⊢ Ⅎ 𝑥 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
11 3 nfel2 ⊢ Ⅎ 𝑦 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴
12 4 nfel2 ⊢ Ⅎ 𝑦 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵
13 11 12 nfbi ⊢ Ⅎ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
14 opeq12 ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ )
15 14 eleq1d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ) )
16 14 eleq1d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ) )
17 15 16 bibi12d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ) ) )
18 6 7 10 13 17 cbval2v ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∀ 𝑢 ∀ 𝑣 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ) )
19 5 18 bitr4di ⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )