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 ∀ z x y z ∈ A → x y z ∈ B

Proof

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