Theorem altopthsn 32068

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

Assertion

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

Proof of Theorem altopthsn

Step	Hyp	Ref	Expression
1		df-altop 32065	. . 3 |- << A , B >> = { { A } , { A , { B } } }
2		df-altop 32065	. . 3 |- << C , D >> = { { C } , { C , { D } } }
3	1, 2	eqeq12i 2636	. 2 |- ( << A , B >> = << C , D >> <-> { { A } , { A , { B } } } = { { C } , { C , { D } } } )
4		snex 4908	. . . . . 6 |- { A } e. _V
5		prex 4909	. . . . . 6 |- { A , { B } } e. _V
6		snex 4908	. . . . . 6 |- { C } e. _V
7		prex 4909	. . . . . 6 |- { C , { D } } e. _V
8	4, 5, 6, 7	preq12b 4382	. . . . 5 |- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } <-> ( ( { A } = { C } /\ { A , { B } } = { C , { D } } ) \/ ( { A } = { C , { D } } /\ { A , { B } } = { C } ) ) )
9		simpl 473	. . . . . 6 |- ( ( { A } = { C } /\ { A , { B } } = { C , { D } } ) -> { A } = { C } )
10		snsspr1 4345	. . . . . . . . 9 |- { A } C_ { A , { B } }
11		sseq2 3627	. . . . . . . . 9 |- ( { A , { B } } = { C } -> ( { A } C_ { A , { B } } <-> { A } C_ { C } ) )
12	10, 11	mpbii 223	. . . . . . . 8 |- ( { A , { B } } = { C } -> { A } C_ { C } )
13	12	adantl 482	. . . . . . 7 |- ( ( { A } = { C , { D } } /\ { A , { B } } = { C } ) -> { A } C_ { C } )
14		snsspr1 4345	. . . . . . . . 9 |- { C } C_ { C , { D } }
15		sseq2 3627	. . . . . . . . 9 |- ( { A } = { C , { D } } -> ( { C } C_ { A } <-> { C } C_ { C , { D } } ) )
16	14, 15	mpbiri 248	. . . . . . . 8 |- ( { A } = { C , { D } } -> { C } C_ { A } )
17	16	adantr 481	. . . . . . 7 |- ( ( { A } = { C , { D } } /\ { A , { B } } = { C } ) -> { C } C_ { A } )
18	13, 17	eqssd 3620	. . . . . 6 |- ( ( { A } = { C , { D } } /\ { A , { B } } = { C } ) -> { A } = { C } )
19	9, 18	jaoi 394	. . . . 5 |- ( ( ( { A } = { C } /\ { A , { B } } = { C , { D } } ) \/ ( { A } = { C , { D } } /\ { A , { B } } = { C } ) ) -> { A } = { C } )
20	8, 19	sylbi 207	. . . 4 |- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } -> { A } = { C } )
21		uneq1 3760	. . . . . . . . . 10 |- ( { A } = { C } -> ( { A } u. { { B } } ) = ( { C } u. { { B } } ) )
22		df-pr 4180	. . . . . . . . . 10 |- { A , { B } } = ( { A } u. { { B } } )
23		df-pr 4180	. . . . . . . . . 10 |- { C , { B } } = ( { C } u. { { B } } )
24	21, 22, 23	3eqtr4g 2681	. . . . . . . . 9 |- ( { A } = { C } -> { A , { B } } = { C , { B } } )
25	24	preq2d 4275	. . . . . . . 8 |- ( { A } = { C } -> { { A } , { A , { B } } } = { { A } , { C , { B } } } )
26		preq1 4268	. . . . . . . 8 |- ( { A } = { C } -> { { A } , { C , { B } } } = { { C } , { C , { B } } } )
27	25, 26	eqtrd 2656	. . . . . . 7 |- ( { A } = { C } -> { { A } , { A , { B } } } = { { C } , { C , { B } } } )
28	27	eqeq1d 2624	. . . . . 6 |- ( { A } = { C } -> ( { { A } , { A , { B } } } = { { C } , { C , { D } } } <-> { { C } , { C , { B } } } = { { C } , { C , { D } } } ) )
29	28	biimpd 219	. . . . 5 |- ( { A } = { C } -> ( { { A } , { A , { B } } } = { { C } , { C , { D } } } -> { { C } , { C , { B } } } = { { C } , { C , { D } } } ) )
30		prex 4909	. . . . . . 7 |- { C , { B } } e. _V
31	30, 7	preqr2 4381	. . . . . 6 |- ( { { C } , { C , { B } } } = { { C } , { C , { D } } } -> { C , { B } } = { C , { D } } )
32		snex 4908	. . . . . . 7 |- { B } e. _V
33		snex 4908	. . . . . . 7 |- { D } e. _V
34	32, 33	preqr2 4381	. . . . . 6 |- ( { C , { B } } = { C , { D } } -> { B } = { D } )
35	31, 34	syl 17	. . . . 5 |- ( { { C } , { C , { B } } } = { { C } , { C , { D } } } -> { B } = { D } )
36	29, 35	syl6com 37	. . . 4 |- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } -> ( { A } = { C } -> { B } = { D } ) )
37	20, 36	jcai 559	. . 3 |- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } -> ( { A } = { C } /\ { B } = { D } ) )
38		preq2 4269	. . . . 5 |- ( { B } = { D } -> { C , { B } } = { C , { D } } )
39	38	preq2d 4275	. . . 4 |- ( { B } = { D } -> { { C } , { C , { B } } } = { { C } , { C , { D } } } )
40	27, 39	sylan9eq 2676	. . 3 |- ( ( { A } = { C } /\ { B } = { D } ) -> { { A } , { A , { B } } } = { { C } , { C , { D } } } )
41	37, 40	impbii 199	. 2 |- ( { { A } , { A , { B } } } = { { C } , { C , { D } } } <-> ( { A } = { C } /\ { B } = { D } ) )
42	3, 41	bitri 264	1 |- ( << A , B >> = << C , D >> <-> ( { A } = { C } /\ { B } = { D } ) )

Syntax hints:   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   u. cun 3572   C_ wss 3574   {csn 4177   {cpr 4179   <<caltop 32063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-altop 32065

This theorem is referenced by:  altopeq12  32069  altopth1  32072  altopth2  32073  altopthg  32074  altopthbg  32075