Metamath Proof Explorer

Theorem eqrelf

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

Ref Expression
Hypotheses eqrelf.1 ⊢ Ⅎ _ x A
eqrelf.2 ⊢ Ⅎ _ x B
eqrelf.3 ⊢ Ⅎ _ y A
eqrelf.4 ⊢ Ⅎ _ y B
Assertion eqrelf ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B ↔ ∀ x ∀ y x y ∈ A ↔ x y ∈ B

Proof

Step Hyp Ref Expression
1 eqrelf.1 ⊢ Ⅎ _ x A
2 eqrelf.2 ⊢ Ⅎ _ x B
3 eqrelf.3 ⊢ Ⅎ _ y A
4 eqrelf.4 ⊢ Ⅎ _ y B
5 eqrel ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B ↔ ∀ u ∀ v u v ∈ A ↔ u v ∈ B
6 nfv ⊢ Ⅎ u x y ∈ A ↔ x y ∈ B
7 nfv ⊢ Ⅎ v x y ∈ A ↔ x y ∈ B
8 1 nfel2 ⊢ Ⅎ x u v ∈ A
9 2 nfel2 ⊢ Ⅎ x u v ∈ B
10 8 9 nfbi ⊢ Ⅎ x u v ∈ A ↔ u v ∈ B
11 3 nfel2 ⊢ Ⅎ y u v ∈ A
12 4 nfel2 ⊢ Ⅎ y u v ∈ B
13 11 12 nfbi ⊢ Ⅎ y u v ∈ A ↔ u v ∈ B
14 opeq12 ⊢ x = u ∧ y = v → x y = u v
15 14 eleq1d ⊢ x = u ∧ y = v → x y ∈ A ↔ u v ∈ A
16 14 eleq1d ⊢ x = u ∧ y = v → x y ∈ B ↔ u v ∈ B
17 15 16 bibi12d ⊢ x = u ∧ y = v → x y ∈ A ↔ x y ∈ B ↔ u v ∈ A ↔ u v ∈ B
18 6 7 10 13 17 cbval2v ⊢ ∀ x ∀ y x y ∈ A ↔ x y ∈ B ↔ ∀ u ∀ v u v ∈ A ↔ u v ∈ B
19 5 18 bitr4di ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B ↔ ∀ x ∀ y x y ∈ A ↔ x y ∈ B