Step 
Hyp 
Ref 
Expression 
1 

dfdju 
 ( A _ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) 
2 
1

eleq2i 
 ( X e. ( A _ B ) <> X e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) ) 
3 

elun 
 ( X e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) <> ( X e. ( { (/) } X. A ) \/ X e. ( { 1o } X. B ) ) ) 
4 
2 3

bitri 
 ( X e. ( A _ B ) <> ( X e. ( { (/) } X. A ) \/ X e. ( { 1o } X. B ) ) ) 
5 

elxp6 
 ( X e. ( { (/) } X. A ) <> ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { (/) } /\ ( 2nd ` X ) e. A ) ) ) 
6 

simprr 
 ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { (/) } /\ ( 2nd ` X ) e. A ) ) > ( 2nd ` X ) e. A ) 
7 
6

a1d 
 ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { (/) } /\ ( 2nd ` X ) e. A ) ) > ( ( 1st ` X ) = (/) > ( 2nd ` X ) e. A ) ) 
8 
5 7

sylbi 
 ( X e. ( { (/) } X. A ) > ( ( 1st ` X ) = (/) > ( 2nd ` X ) e. A ) ) 
9 

elxp6 
 ( X e. ( { 1o } X. B ) <> ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { 1o } /\ ( 2nd ` X ) e. B ) ) ) 
10 

elsni 
 ( ( 1st ` X ) e. { 1o } > ( 1st ` X ) = 1o ) 
11 

1n0 
 1o =/= (/) 
12 

neeq1 
 ( ( 1st ` X ) = 1o > ( ( 1st ` X ) =/= (/) <> 1o =/= (/) ) ) 
13 
11 12

mpbiri 
 ( ( 1st ` X ) = 1o > ( 1st ` X ) =/= (/) ) 
14 

eqneqall 
 ( ( 1st ` X ) = (/) > ( ( 1st ` X ) =/= (/) > ( 2nd ` X ) e. A ) ) 
15 
14

com12 
 ( ( 1st ` X ) =/= (/) > ( ( 1st ` X ) = (/) > ( 2nd ` X ) e. A ) ) 
16 
10 13 15

3syl 
 ( ( 1st ` X ) e. { 1o } > ( ( 1st ` X ) = (/) > ( 2nd ` X ) e. A ) ) 
17 
16

ad2antrl 
 ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { 1o } /\ ( 2nd ` X ) e. B ) ) > ( ( 1st ` X ) = (/) > ( 2nd ` X ) e. A ) ) 
18 
9 17

sylbi 
 ( X e. ( { 1o } X. B ) > ( ( 1st ` X ) = (/) > ( 2nd ` X ) e. A ) ) 
19 
8 18

jaoi 
 ( ( X e. ( { (/) } X. A ) \/ X e. ( { 1o } X. B ) ) > ( ( 1st ` X ) = (/) > ( 2nd ` X ) e. A ) ) 
20 
4 19

sylbi 
 ( X e. ( A _ B ) > ( ( 1st ` X ) = (/) > ( 2nd ` X ) e. A ) ) 
21 
20

imp 
 ( ( X e. ( A _ B ) /\ ( 1st ` X ) = (/) ) > ( 2nd ` X ) e. A ) 