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

Metamath Proof Explorer

Theorem eqrelrel

Description: Extensionality principle for ordered triples (used by 2-place operations df-oprab ), analogous to eqrel . Use relrelss to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008)

Ref Expression
Assertion eqrelrel ⊢ A ∪ B ⊆ V × V × V → A = B ↔ ∀ x ∀ y ∀ z x y z ∈ A ↔ x y z ∈ B

Proof

Step Hyp Ref Expression
1 unss ⊢ A ⊆ V × V × V ∧ B ⊆ V × V × V ↔ A ∪ B ⊆ V × V × V
2 ssrelrel ⊢ A ⊆ V × V × V → A ⊆ B ↔ ∀ x ∀ y ∀ z x y z ∈ A → x y z ∈ B
3 ssrelrel ⊢ B ⊆ V × V × V → B ⊆ A ↔ ∀ x ∀ y ∀ z x y z ∈ B → x y z ∈ A
4 2 3 bi2anan9 ⊢ A ⊆ V × V × V ∧ B ⊆ V × V × V → A ⊆ B ∧ B ⊆ A ↔ ∀ x ∀ y ∀ z x y z ∈ A → x y z ∈ B ∧ ∀ x ∀ y ∀ z x y z ∈ B → x y z ∈ A
5 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
6 2albiim ⊢ ∀ y ∀ z x y z ∈ A ↔ x y z ∈ B ↔ ∀ y ∀ z x y z ∈ A → x y z ∈ B ∧ ∀ y ∀ z x y z ∈ B → x y z ∈ A
7 6 albii ⊢ ∀ x ∀ y ∀ z x y z ∈ A ↔ x y z ∈ B ↔ ∀ x ∀ y ∀ z x y z ∈ A → x y z ∈ B ∧ ∀ y ∀ z x y z ∈ B → x y z ∈ A
8 19.26 ⊢ ∀ x ∀ y ∀ z x y z ∈ A → x y z ∈ B ∧ ∀ y ∀ z x y z ∈ B → x y z ∈ A ↔ ∀ x ∀ y ∀ z x y z ∈ A → x y z ∈ B ∧ ∀ x ∀ y ∀ z x y z ∈ B → x y z ∈ A
9 7 8 bitri ⊢ ∀ x ∀ y ∀ z x y z ∈ A ↔ x y z ∈ B ↔ ∀ x ∀ y ∀ z x y z ∈ A → x y z ∈ B ∧ ∀ x ∀ y ∀ z x y z ∈ B → x y z ∈ A
10 4 5 9 3bitr4g ⊢ A ⊆ V × V × V ∧ B ⊆ V × V × V → A = B ↔ ∀ x ∀ y ∀ z x y z ∈ A ↔ x y z ∈ B
11 1 10 sylbir ⊢ A ∪ B ⊆ V × V × V → A = B ↔ ∀ x ∀ y ∀ z x y z ∈ A ↔ x y z ∈ B