Metamath Proof Explorer

Theorem eqrel2

Description: Equality of relations. (Contributed by Peter Mazsa, 8-Mar-2019)

Ref Expression
Assertion eqrel2 ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B ↔ ∀ x ∀ y x A y ↔ x B y

Proof

Step Hyp Ref Expression
1 ssrel3 ⊢ Rel ⁡ A → A ⊆ B ↔ ∀ x ∀ y x A y → x B y
2 ssrel3 ⊢ Rel ⁡ B → B ⊆ A ↔ ∀ x ∀ y x B y → x A y
3 1 2 bi2anan9 ⊢ Rel ⁡ A ∧ Rel ⁡ B → A ⊆ B ∧ B ⊆ A ↔ ∀ x ∀ y x A y → x B y ∧ ∀ x ∀ y x B y → x A y
4 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
5 2albiim ⊢ ∀ x ∀ y x A y ↔ x B y ↔ ∀ x ∀ y x A y → x B y ∧ ∀ x ∀ y x B y → x A y
6 3 4 5 3bitr4g ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B ↔ ∀ x ∀ y x A y ↔ x B y