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∀zxyz∈A↔xyz∈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∀zxyz∈A→xyz∈B
3 ssrelrel ⊢B⊆V×V×V→B⊆A↔∀x∀y∀zxyz∈B→xyz∈A
4 2 3 bi2anan9 ⊢A⊆V×V×V∧B⊆V×V×V→A⊆B∧B⊆A↔∀x∀y∀zxyz∈A→xyz∈B∧∀x∀y∀zxyz∈B→xyz∈A
5 eqss ⊢A=B↔A⊆B∧B⊆A
6 2albiim ⊢∀y∀zxyz∈A↔xyz∈B↔∀y∀zxyz∈A→xyz∈B∧∀y∀zxyz∈B→xyz∈A
7 6 albii ⊢∀x∀y∀zxyz∈A↔xyz∈B↔∀x∀y∀zxyz∈A→xyz∈B∧∀y∀zxyz∈B→xyz∈A
8 19.26 ⊢∀x∀y∀zxyz∈A→xyz∈B∧∀y∀zxyz∈B→xyz∈A↔∀x∀y∀zxyz∈A→xyz∈B∧∀x∀y∀zxyz∈B→xyz∈A
9 7 8 bitri ⊢∀x∀y∀zxyz∈A↔xyz∈B↔∀x∀y∀zxyz∈A→xyz∈B∧∀x∀y∀zxyz∈B→xyz∈A
10 4 5 9 3bitr4g ⊢A⊆V×V×V∧B⊆V×V×V→A=B↔∀x∀y∀zxyz∈A↔xyz∈B
11 1 10 sylbir ⊢A∪B⊆V×V×V→A=B↔∀x∀y∀zxyz∈A↔xyz∈B