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