Metamath Proof Explorer

Theorem eqrel

Description: Extensionality principle for relations. Theorem 3.2(ii) of Monk1 p. 33. (Contributed by NM, 2-Aug-1994)

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

Proof

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