Metamath Proof Explorer

Theorem ssrelrel

Description: A subclass relationship determined by ordered triples. Use relrelss to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion ssrelrel ⊢A⊆V×V×V→A⊆B↔∀x∀y∀zxyz∈A→xyz∈B

Proof

Step Hyp Ref Expression
1 ssel ⊢A⊆B→xyz∈A→xyz∈B
2 1 alrimiv ⊢A⊆B→∀zxyz∈A→xyz∈B
3 2 alrimivv ⊢A⊆B→∀x∀y∀zxyz∈A→xyz∈B
4 elvvv ⊢w∈V×V×V↔∃x∃y∃zw=xyz
5 eleq1 ⊢w=xyz→w∈A↔xyz∈A
6 eleq1 ⊢w=xyz→w∈B↔xyz∈B
7 5 6 imbi12d ⊢w=xyz→w∈A→w∈B↔xyz∈A→xyz∈B
8 7 biimprcd ⊢xyz∈A→xyz∈B→w=xyz→w∈A→w∈B
9 8 alimi ⊢∀zxyz∈A→xyz∈B→∀zw=xyz→w∈A→w∈B
10 19.23v ⊢∀zw=xyz→w∈A→w∈B↔∃zw=xyz→w∈A→w∈B
11 9 10 sylib ⊢∀zxyz∈A→xyz∈B→∃zw=xyz→w∈A→w∈B
12 11 2alimi ⊢∀x∀y∀zxyz∈A→xyz∈B→∀x∀y∃zw=xyz→w∈A→w∈B
13 19.23vv ⊢∀x∀y∃zw=xyz→w∈A→w∈B↔∃x∃y∃zw=xyz→w∈A→w∈B
14 12 13 sylib ⊢∀x∀y∀zxyz∈A→xyz∈B→∃x∃y∃zw=xyz→w∈A→w∈B
15 4 14 biimtrid ⊢∀x∀y∀zxyz∈A→xyz∈B→w∈V×V×V→w∈A→w∈B
16 15 com23 ⊢∀x∀y∀zxyz∈A→xyz∈B→w∈A→w∈V×V×V→w∈B
17 16 a2d ⊢∀x∀y∀zxyz∈A→xyz∈B→w∈A→w∈V×V×V→w∈A→w∈B
18 17 alimdv ⊢∀x∀y∀zxyz∈A→xyz∈B→∀ww∈A→w∈V×V×V→∀ww∈A→w∈B
19 dfss2 ⊢A⊆V×V×V↔∀ww∈A→w∈V×V×V
20 dfss2 ⊢A⊆B↔∀ww∈A→w∈B
21 18 19 20 3imtr4g ⊢∀x∀y∀zxyz∈A→xyz∈B→A⊆V×V×V→A⊆B
22 21 com12 ⊢A⊆V×V×V→∀x∀y∀zxyz∈A→xyz∈B→A⊆B
23 3 22 impbid2 ⊢A⊆V×V×V→A⊆B↔∀x∀y∀zxyz∈A→xyz∈B