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 ( ( 𝐴 ∪ 𝐵 ) ⊆ ( ( V × V ) × V ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 unss ⊢ ( ( 𝐴 ⊆ ( ( V × V ) × V ) ∧ 𝐵 ⊆ ( ( V × V ) × V ) ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( ( V × V ) × V ) )
2 ssrelrel ⊢ ( 𝐴 ⊆ ( ( V × V ) × V ) → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ) )
3 ssrelrel ⊢ ( 𝐵 ⊆ ( ( V × V ) × V ) → ( 𝐵 ⊆ 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ) ) )
4 2 3 bi2anan9 ⊢ ( ( 𝐴 ⊆ ( ( V × V ) × V ) ∧ 𝐵 ⊆ ( ( V × V ) × V ) ) → ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ) ) ) )
5 eqss ⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
6 2albiim ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ↔ ( ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ∧ ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ) ) )
7 6 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ↔ ∀ 𝑥 ( ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ∧ ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ) ) )
8 19.26 ⊢ ( ∀ 𝑥 ( ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ∧ ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ) ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ) ) )
9 7 8 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ) ) )
10 4 5 9 3bitr4g ⊢ ( ( 𝐴 ⊆ ( ( V × V ) × V ) ∧ 𝐵 ⊆ ( ( V × V ) × V ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ) )
11 1 10 sylbir ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( ( V × V ) × V ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐴 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐵 ) ) )