Metamath Proof Explorer

Theorem sseliALT

Description: Alternate proof of sseli illustrating the use of the weak deduction theorem to prove it from the inference sselii . (Contributed by NM, 24-Aug-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis sseliALT.1 ⊢ A ⊆ B
Assertion sseliALT ⊢ C ∈ A → C ∈ B

Proof

Step Hyp Ref Expression
1 sseliALT.1 ⊢ A ⊆ B
2 biidd ⊢ A = if C ∈ A A ∅ → C ∈ B ↔ C ∈ B
3 eleq2 ⊢ B = if C ∈ A B ∅ → C ∈ B ↔ C ∈ if C ∈ A B ∅
4 eleq1 ⊢ C = if C ∈ A C ∅ → C ∈ if C ∈ A B ∅ ↔ if C ∈ A C ∅ ∈ if C ∈ A B ∅
5 sseq1 ⊢ A = if C ∈ A A ∅ → A ⊆ B ↔ if C ∈ A A ∅ ⊆ B
6 sseq2 ⊢ B = if C ∈ A B ∅ → if C ∈ A A ∅ ⊆ B ↔ if C ∈ A A ∅ ⊆ if C ∈ A B ∅
7 biidd ⊢ C = if C ∈ A C ∅ → if C ∈ A A ∅ ⊆ if C ∈ A B ∅ ↔ if C ∈ A A ∅ ⊆ if C ∈ A B ∅
8 sseq1 ⊢ ∅ = if C ∈ A A ∅ → ∅ ⊆ ∅ ↔ if C ∈ A A ∅ ⊆ ∅
9 sseq2 ⊢ ∅ = if C ∈ A B ∅ → if C ∈ A A ∅ ⊆ ∅ ↔ if C ∈ A A ∅ ⊆ if C ∈ A B ∅
10 biidd ⊢ ∅ = if C ∈ A C ∅ → if C ∈ A A ∅ ⊆ if C ∈ A B ∅ ↔ if C ∈ A A ∅ ⊆ if C ∈ A B ∅
11 ssid ⊢ ∅ ⊆ ∅
12 5 6 7 8 9 10 1 11 keephyp3v ⊢ if C ∈ A A ∅ ⊆ if C ∈ A B ∅
13 eleq2 ⊢ A = if C ∈ A A ∅ → C ∈ A ↔ C ∈ if C ∈ A A ∅
14 biidd ⊢ B = if C ∈ A B ∅ → C ∈ if C ∈ A A ∅ ↔ C ∈ if C ∈ A A ∅
15 eleq1 ⊢ C = if C ∈ A C ∅ → C ∈ if C ∈ A A ∅ ↔ if C ∈ A C ∅ ∈ if C ∈ A A ∅
16 eleq2 ⊢ ∅ = if C ∈ A A ∅ → ∅ ∈ ∅ ↔ ∅ ∈ if C ∈ A A ∅
17 biidd ⊢ ∅ = if C ∈ A B ∅ → ∅ ∈ if C ∈ A A ∅ ↔ ∅ ∈ if C ∈ A A ∅
18 eleq1 ⊢ ∅ = if C ∈ A C ∅ → ∅ ∈ if C ∈ A A ∅ ↔ if C ∈ A C ∅ ∈ if C ∈ A A ∅
19 0ex ⊢ ∅ ∈ V
20 19 snid ⊢ ∅ ∈ ∅
21 13 14 15 16 17 18 20 elimhyp3v ⊢ if C ∈ A C ∅ ∈ if C ∈ A A ∅
22 12 21 sselii ⊢ if C ∈ A C ∅ ∈ if C ∈ A B ∅
23 2 3 4 22 dedth3v ⊢ C ∈ A → C ∈ B