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 ) ) ) )