Theorem altopthsn

Description: Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	altopthsn	|- ( << A , B >> = << C , D >> <-> ( { A } = { C } /\ { B } = { D } ) )

Proof

Step	Hyp	Ref	Expression
1		df-altop	|- << A , B >> = { { A } , { A , { B } } }
2		df-altop	|- << C , D >> = { { C } , { C , { D } } }
3	1 2	eqeq12i	|- ( << A , B >> = << C , D >> <-> { { A } , { A , { B } } } = { { C } , { C , { D } } } )
4		snex	|- { A } e. _V
5		prex	|- { A , { B } } e. _V
6		snex	|- { C } e. _V
7		prex	|- { C , { D } } e. _V
8	4 5 6 7	preq12b	|- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } <-> ( ( { A } = { C } /\ { A , { B } } = { C , { D } } ) \/ ( { A } = { C , { D } } /\ { A , { B } } = { C } ) ) )
9		simpl	|- ( ( { A } = { C } /\ { A , { B } } = { C , { D } } ) -> { A } = { C } )
10		snsspr1	|- { A } C_ { A , { B } }
11		sseq2	|- ( { A , { B } } = { C } -> ( { A } C_ { A , { B } } <-> { A } C_ { C } ) )
12	10 11	mpbii	|- ( { A , { B } } = { C } -> { A } C_ { C } )
13	12	adantl	|- ( ( { A } = { C , { D } } /\ { A , { B } } = { C } ) -> { A } C_ { C } )
14		snsspr1	|- { C } C_ { C , { D } }
15		sseq2	|- ( { A } = { C , { D } } -> ( { C } C_ { A } <-> { C } C_ { C , { D } } ) )
16	14 15	mpbiri	|- ( { A } = { C , { D } } -> { C } C_ { A } )
17	16	adantr	|- ( ( { A } = { C , { D } } /\ { A , { B } } = { C } ) -> { C } C_ { A } )
18	13 17	eqssd	|- ( ( { A } = { C , { D } } /\ { A , { B } } = { C } ) -> { A } = { C } )
19	9 18	jaoi	|- ( ( ( { A } = { C } /\ { A , { B } } = { C , { D } } ) \/ ( { A } = { C , { D } } /\ { A , { B } } = { C } ) ) -> { A } = { C } )
20	8 19	sylbi	|- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } -> { A } = { C } )
21		uneq1	|- ( { A } = { C } -> ( { A } u. { { B } } ) = ( { C } u. { { B } } ) )
22		df-pr	|- { A , { B } } = ( { A } u. { { B } } )
23		df-pr	|- { C , { B } } = ( { C } u. { { B } } )
24	21 22 23	3eqtr4g	|- ( { A } = { C } -> { A , { B } } = { C , { B } } )
25	24	preq2d	|- ( { A } = { C } -> { { A } , { A , { B } } } = { { A } , { C , { B } } } )
26		preq1	|- ( { A } = { C } -> { { A } , { C , { B } } } = { { C } , { C , { B } } } )
27	25 26	eqtrd	|- ( { A } = { C } -> { { A } , { A , { B } } } = { { C } , { C , { B } } } )
28	27	eqeq1d	|- ( { A } = { C } -> ( { { A } , { A , { B } } } = { { C } , { C , { D } } } <-> { { C } , { C , { B } } } = { { C } , { C , { D } } } ) )
29	28	biimpd	|- ( { A } = { C } -> ( { { A } , { A , { B } } } = { { C } , { C , { D } } } -> { { C } , { C , { B } } } = { { C } , { C , { D } } } ) )
30		prex	|- { C , { B } } e. _V
31	30 7	preqr2	|- ( { { C } , { C , { B } } } = { { C } , { C , { D } } } -> { C , { B } } = { C , { D } } )
32		snex	|- { B } e. _V
33		snex	|- { D } e. _V
34	32 33	preqr2	|- ( { C , { B } } = { C , { D } } -> { B } = { D } )
35	31 34	syl	|- ( { { C } , { C , { B } } } = { { C } , { C , { D } } } -> { B } = { D } )
36	29 35	syl6com	|- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } -> ( { A } = { C } -> { B } = { D } ) )
37	20 36	jcai	|- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } -> ( { A } = { C } /\ { B } = { D } ) )
38		preq2	|- ( { B } = { D } -> { C , { B } } = { C , { D } } )
39	38	preq2d	|- ( { B } = { D } -> { { C } , { C , { B } } } = { { C } , { C , { D } } } )
40	27 39	sylan9eq	|- ( ( { A } = { C } /\ { B } = { D } ) -> { { A } , { A , { B } } } = { { C } , { C , { D } } } )
41	37 40	impbii	|- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } <-> ( { A } = { C } /\ { B } = { D } ) )
42	3 41	bitri	|- ( << A , B >> = << C , D >> <-> ( { A } = { C } /\ { B } = { D } ) )