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=ifC∈AA∅→C∈B↔C∈B
3 eleq2 ⊢B=ifC∈AB∅→C∈B↔C∈ifC∈AB∅
4 eleq1 ⊢C=ifC∈AC∅→C∈ifC∈AB∅↔ifC∈AC∅∈ifC∈AB∅
5 sseq1 ⊢A=ifC∈AA∅→A⊆B↔ifC∈AA∅⊆B
6 sseq2 ⊢B=ifC∈AB∅→ifC∈AA∅⊆B↔ifC∈AA∅⊆ifC∈AB∅
7 biidd ⊢C=ifC∈AC∅→ifC∈AA∅⊆ifC∈AB∅↔ifC∈AA∅⊆ifC∈AB∅
8 sseq1 ⊢∅=ifC∈AA∅→∅⊆∅↔ifC∈AA∅⊆∅
9 sseq2 ⊢∅=ifC∈AB∅→ifC∈AA∅⊆∅↔ifC∈AA∅⊆ifC∈AB∅
10 biidd ⊢∅=ifC∈AC∅→ifC∈AA∅⊆ifC∈AB∅↔ifC∈AA∅⊆ifC∈AB∅
11 ssid ⊢∅⊆∅
12 5 6 7 8 9 10 1 11 keephyp3v ⊢ifC∈AA∅⊆ifC∈AB∅
13 eleq2 ⊢A=ifC∈AA∅→C∈A↔C∈ifC∈AA∅
14 biidd ⊢B=ifC∈AB∅→C∈ifC∈AA∅↔C∈ifC∈AA∅
15 eleq1 ⊢C=ifC∈AC∅→C∈ifC∈AA∅↔ifC∈AC∅∈ifC∈AA∅
16 eleq2 ⊢∅=ifC∈AA∅→∅∈∅↔∅∈ifC∈AA∅
17 biidd ⊢∅=ifC∈AB∅→∅∈ifC∈AA∅↔∅∈ifC∈AA∅
18 eleq1 ⊢∅=ifC∈AC∅→∅∈ifC∈AA∅↔ifC∈AC∅∈ifC∈AA∅
19 0ex ⊢∅∈V
20 19 snid ⊢∅∈∅
21 13 14 15 16 17 18 20 elimhyp3v ⊢ifC∈AC∅∈ifC∈AA∅
22 12 21 sselii ⊢ifC∈AC∅∈ifC∈AB∅
23 2 3 4 22 dedth3v ⊢C∈A→C∈B