Theorem en2eqpr

Description: Building a set with two elements. (Contributed by FL, 11-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	en2eqpr	|- ( ( C ~~ 2o /\ A e. C /\ B e. C ) -> ( A =/= B -> C = { A , B } ) )

Proof

Step	Hyp	Ref	Expression
1		2onn	|- 2o e. _om
2		nnfi	|- ( 2o e. _om -> 2o e. Fin )
3	1 2	ax-mp	|- 2o e. Fin
4		simpl1	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> C ~~ 2o )
5		enfii	|- ( ( 2o e. Fin /\ C ~~ 2o ) -> C e. Fin )
6	3 4 5	sylancr	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> C e. Fin )
7		simpl2	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> A e. C )
8		simpl3	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> B e. C )
9	7 8	prssd	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> { A , B } C_ C )
10		pr2nelem	|- ( ( A e. C /\ B e. C /\ A =/= B ) -> { A , B } ~~ 2o )
11	10	3expa	|- ( ( ( A e. C /\ B e. C ) /\ A =/= B ) -> { A , B } ~~ 2o )
12	11	3adantl1	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> { A , B } ~~ 2o )
13	4	ensymd	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> 2o ~~ C )
14		entr	|- ( ( { A , B } ~~ 2o /\ 2o ~~ C ) -> { A , B } ~~ C )
15	12 13 14	syl2anc	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> { A , B } ~~ C )
16		fisseneq	|- ( ( C e. Fin /\ { A , B } C_ C /\ { A , B } ~~ C ) -> { A , B } = C )
17	6 9 15 16	syl3anc	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> { A , B } = C )
18	17	eqcomd	|- ( ( ( C ~~ 2o /\ A e. C /\ B e. C ) /\ A =/= B ) -> C = { A , B } )
19	18	ex	|- ( ( C ~~ 2o /\ A e. C /\ B e. C ) -> ( A =/= B -> C = { A , B } ) )