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 C_ B
Assertion sseliALT 
|- ( C e. A -> C e. B )

Proof

Step Hyp Ref Expression
1 sseliALT.1 
 |-  A C_ B
2 biidd 
 |-  ( A = if ( C e. A , A , { (/) } ) -> ( C e. B <-> C e. B ) )
3 eleq2 
 |-  ( B = if ( C e. A , B , { (/) } ) -> ( C e. B <-> C e. if ( C e. A , B , { (/) } ) ) )
4 eleq1 
 |-  ( C = if ( C e. A , C , (/) ) -> ( C e. if ( C e. A , B , { (/) } ) <-> if ( C e. A , C , (/) ) e. if ( C e. A , B , { (/) } ) ) )
5 sseq1 
 |-  ( A = if ( C e. A , A , { (/) } ) -> ( A C_ B <-> if ( C e. A , A , { (/) } ) C_ B ) )
6 sseq2 
 |-  ( B = if ( C e. A , B , { (/) } ) -> ( if ( C e. A , A , { (/) } ) C_ B <-> if ( C e. A , A , { (/) } ) C_ if ( C e. A , B , { (/) } ) ) )
7 biidd 
 |-  ( C = if ( C e. A , C , (/) ) -> ( if ( C e. A , A , { (/) } ) C_ if ( C e. A , B , { (/) } ) <-> if ( C e. A , A , { (/) } ) C_ if ( C e. A , B , { (/) } ) ) )
8 sseq1 
 |-  ( { (/) } = if ( C e. A , A , { (/) } ) -> ( { (/) } C_ { (/) } <-> if ( C e. A , A , { (/) } ) C_ { (/) } ) )
9 sseq2 
 |-  ( { (/) } = if ( C e. A , B , { (/) } ) -> ( if ( C e. A , A , { (/) } ) C_ { (/) } <-> if ( C e. A , A , { (/) } ) C_ if ( C e. A , B , { (/) } ) ) )
10 biidd 
 |-  ( (/) = if ( C e. A , C , (/) ) -> ( if ( C e. A , A , { (/) } ) C_ if ( C e. A , B , { (/) } ) <-> if ( C e. A , A , { (/) } ) C_ if ( C e. A , B , { (/) } ) ) )
11 ssid 
 |-  { (/) } C_ { (/) }
12 5 6 7 8 9 10 1 11 keephyp3v 
 |-  if ( C e. A , A , { (/) } ) C_ if ( C e. A , B , { (/) } )
13 eleq2 
 |-  ( A = if ( C e. A , A , { (/) } ) -> ( C e. A <-> C e. if ( C e. A , A , { (/) } ) ) )
14 biidd 
 |-  ( B = if ( C e. A , B , { (/) } ) -> ( C e. if ( C e. A , A , { (/) } ) <-> C e. if ( C e. A , A , { (/) } ) ) )
15 eleq1 
 |-  ( C = if ( C e. A , C , (/) ) -> ( C e. if ( C e. A , A , { (/) } ) <-> if ( C e. A , C , (/) ) e. if ( C e. A , A , { (/) } ) ) )
16 eleq2 
 |-  ( { (/) } = if ( C e. A , A , { (/) } ) -> ( (/) e. { (/) } <-> (/) e. if ( C e. A , A , { (/) } ) ) )
17 biidd 
 |-  ( { (/) } = if ( C e. A , B , { (/) } ) -> ( (/) e. if ( C e. A , A , { (/) } ) <-> (/) e. if ( C e. A , A , { (/) } ) ) )
18 eleq1 
 |-  ( (/) = if ( C e. A , C , (/) ) -> ( (/) e. if ( C e. A , A , { (/) } ) <-> if ( C e. A , C , (/) ) e. if ( C e. A , A , { (/) } ) ) )
19 0ex 
 |-  (/) e. _V
20 19 snid 
 |-  (/) e. { (/) }
21 13 14 15 16 17 18 20 elimhyp3v 
 |-  if ( C e. A , C , (/) ) e. if ( C e. A , A , { (/) } )
22 12 21 sselii 
 |-  if ( C e. A , C , (/) ) e. if ( C e. A , B , { (/) } )
23 2 3 4 22 dedth3v 
 |-  ( C e. A -> C e. B )