This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eupth2lem1

Description: Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015)

Ref Expression
Assertion eupth2lem1 
|- ( U e. V -> ( U e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( (/) = if ( A = B , (/) , { A , B } ) -> ( U e. (/) <-> U e. if ( A = B , (/) , { A , B } ) ) )
2 1 bibi1d 
 |-  ( (/) = if ( A = B , (/) , { A , B } ) -> ( ( U e. (/) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) <-> ( U e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) ) )
3 eleq2 
 |-  ( { A , B } = if ( A = B , (/) , { A , B } ) -> ( U e. { A , B } <-> U e. if ( A = B , (/) , { A , B } ) ) )
4 3 bibi1d 
 |-  ( { A , B } = if ( A = B , (/) , { A , B } ) -> ( ( U e. { A , B } <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) <-> ( U e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) ) )
5 noel 
 |-  -. U e. (/)
6 5 a1i 
 |-  ( ( U e. V /\ A = B ) -> -. U e. (/) )
7 simpl 
 |-  ( ( A =/= B /\ ( U = A \/ U = B ) ) -> A =/= B )
8 7 neneqd 
 |-  ( ( A =/= B /\ ( U = A \/ U = B ) ) -> -. A = B )
9 simpr 
 |-  ( ( U e. V /\ A = B ) -> A = B )
10 8 9 nsyl3 
 |-  ( ( U e. V /\ A = B ) -> -. ( A =/= B /\ ( U = A \/ U = B ) ) )
11 6 10 2falsed 
 |-  ( ( U e. V /\ A = B ) -> ( U e. (/) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) )
12 elprg 
 |-  ( U e. V -> ( U e. { A , B } <-> ( U = A \/ U = B ) ) )
13 df-ne 
 |-  ( A =/= B <-> -. A = B )
14 ibar 
 |-  ( A =/= B -> ( ( U = A \/ U = B ) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) )
15 13 14 sylbir 
 |-  ( -. A = B -> ( ( U = A \/ U = B ) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) )
16 12 15 sylan9bb 
 |-  ( ( U e. V /\ -. A = B ) -> ( U e. { A , B } <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) )
17 2 4 11 16 ifbothda 
 |-  ( U e. V -> ( U e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) )