Theorem elsprel 41725

Description: An unordered pair is an element of all unordered pairs. At least one of the two elements of the unordered pair must be a set. Otherwise, the unordered pair would be the empty set, see prprc 4302, which is not an element of all unordered pairs, see spr0nelg 41726. (Contributed by AV, 21-Nov-2021.)

Assertion

Ref	Expression
elsprel	|- ( ( A e. V \/ B e. W ) -> { A , B } e. { p | E. a E. b p = { a , b } } )

Distinct variable groups:   A, a, b, p   B, a, b, p

Allowed substitution hints:   V( p, a, b)   W( p, a, b)

Proof of Theorem elsprel

Step	Hyp	Ref	Expression
1		elex 3212	. . . 4 |- ( A e. V -> A e. _V )
2		elex 3212	. . . 4 |- ( B e. W -> B e. _V )
3	1, 2	orim12i 538	. . 3 |- ( ( A e. V \/ B e. W ) -> ( A e. _V \/ B e. _V ) )
4		elisset 3215	. . . . . . 7 |- ( A e. _V -> E. a a = A )
5		elisset 3215	. . . . . . 7 |- ( B e. _V -> E. b b = B )
6		eeanv 2182	. . . . . . . 8 |- ( E. a E. b ( a = A /\ b = B ) <-> ( E. a a = A /\ E. b b = B ) )
7		preq12 4270	. . . . . . . . . 10 |- ( ( a = A /\ b = B ) -> { a , b } = { A , B } )
8	7	eqcomd 2628	. . . . . . . . 9 |- ( ( a = A /\ b = B ) -> { A , B } = { a , b } )
9	8	2eximi 1763	. . . . . . . 8 |- ( E. a E. b ( a = A /\ b = B ) -> E. a E. b { A , B } = { a , b } )
10	6, 9	sylbir 225	. . . . . . 7 |- ( ( E. a a = A /\ E. b b = B ) -> E. a E. b { A , B } = { a , b } )
11	4, 5, 10	syl2an 494	. . . . . 6 |- ( ( A e. _V /\ B e. _V ) -> E. a E. b { A , B } = { a , b } )
12	11	expcom 451	. . . . 5 |- ( B e. _V -> ( A e. _V -> E. a E. b { A , B } = { a , b } ) )
13		preq2 4269	. . . . . . . . . . . . . 14 |- ( b = a -> { a , b } = { a , a } )
14	13	adantr 481	. . . . . . . . . . . . 13 |- ( ( b = a /\ a = A ) -> { a , b } = { a , a } )
15		dfsn2 4190	. . . . . . . . . . . . . 14 |- { a } = { a , a }
16		sneq 4187	. . . . . . . . . . . . . . 15 |- ( a = A -> { a } = { A } )
17	16	adantl 482	. . . . . . . . . . . . . 14 |- ( ( b = a /\ a = A ) -> { a } = { A } )
18	15, 17	syl5eqr 2670	. . . . . . . . . . . . 13 |- ( ( b = a /\ a = A ) -> { a , a } = { A } )
19	14, 18	eqtr2d 2657	. . . . . . . . . . . 12 |- ( ( b = a /\ a = A ) -> { A } = { a , b } )
20	19	ex 450	. . . . . . . . . . 11 |- ( b = a -> ( a = A -> { A } = { a , b } ) )
21	20	spimev 2259	. . . . . . . . . 10 |- ( a = A -> E. b { A } = { a , b } )
22	21	adantl 482	. . . . . . . . 9 |- ( ( -. B e. _V /\ a = A ) -> E. b { A } = { a , b } )
23		prprc2 4301	. . . . . . . . . . . 12 |- ( -. B e. _V -> { A , B } = { A } )
24	23	adantr 481	. . . . . . . . . . 11 |- ( ( -. B e. _V /\ a = A ) -> { A , B } = { A } )
25	24	eqeq1d 2624	. . . . . . . . . 10 |- ( ( -. B e. _V /\ a = A ) -> ( { A , B } = { a , b } <-> { A } = { a , b } ) )
26	25	exbidv 1850	. . . . . . . . 9 |- ( ( -. B e. _V /\ a = A ) -> ( E. b { A , B } = { a , b } <-> E. b { A } = { a , b } ) )
27	22, 26	mpbird 247	. . . . . . . 8 |- ( ( -. B e. _V /\ a = A ) -> E. b { A , B } = { a , b } )
28	27	ex 450	. . . . . . 7 |- ( -. B e. _V -> ( a = A -> E. b { A , B } = { a , b } ) )
29	28	eximdv 1846	. . . . . 6 |- ( -. B e. _V -> ( E. a a = A -> E. a E. b { A , B } = { a , b } ) )
30	4, 29	syl5 34	. . . . 5 |- ( -. B e. _V -> ( A e. _V -> E. a E. b { A , B } = { a , b } ) )
31	12, 30	pm2.61i 176	. . . 4 |- ( A e. _V -> E. a E. b { A , B } = { a , b } )
32	11	ex 450	. . . . 5 |- ( A e. _V -> ( B e. _V -> E. a E. b { A , B } = { a , b } ) )
33		preq1 4268	. . . . . . . . . . . . . . . . 17 |- ( a = b -> { a , b } = { b , b } )
34	33	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( a = b /\ b = B ) -> { a , b } = { b , b } )
35		dfsn2 4190	. . . . . . . . . . . . . . . . 17 |- { b } = { b , b }
36		sneq 4187	. . . . . . . . . . . . . . . . . 18 |- ( b = B -> { b } = { B } )
37	36	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( a = b /\ b = B ) -> { b } = { B } )
38	35, 37	syl5eqr 2670	. . . . . . . . . . . . . . . 16 |- ( ( a = b /\ b = B ) -> { b , b } = { B } )
39	34, 38	eqtr2d 2657	. . . . . . . . . . . . . . 15 |- ( ( a = b /\ b = B ) -> { B } = { a , b } )
40	39	ex 450	. . . . . . . . . . . . . 14 |- ( a = b -> ( b = B -> { B } = { a , b } ) )
41	40	spimev 2259	. . . . . . . . . . . . 13 |- ( b = B -> E. a { B } = { a , b } )
42	41	adantl 482	. . . . . . . . . . . 12 |- ( ( -. A e. _V /\ b = B ) -> E. a { B } = { a , b } )
43		prprc1 4300	. . . . . . . . . . . . . . 15 |- ( -. A e. _V -> { A , B } = { B } )
44	43	adantr 481	. . . . . . . . . . . . . 14 |- ( ( -. A e. _V /\ b = B ) -> { A , B } = { B } )
45	44	eqeq1d 2624	. . . . . . . . . . . . 13 |- ( ( -. A e. _V /\ b = B ) -> ( { A , B } = { a , b } <-> { B } = { a , b } ) )
46	45	exbidv 1850	. . . . . . . . . . . 12 |- ( ( -. A e. _V /\ b = B ) -> ( E. a { A , B } = { a , b } <-> E. a { B } = { a , b } ) )
47	42, 46	mpbird 247	. . . . . . . . . . 11 |- ( ( -. A e. _V /\ b = B ) -> E. a { A , B } = { a , b } )
48	47	ex 450	. . . . . . . . . 10 |- ( -. A e. _V -> ( b = B -> E. a { A , B } = { a , b } ) )
49	48	eximdv 1846	. . . . . . . . 9 |- ( -. A e. _V -> ( E. b b = B -> E. b E. a { A , B } = { a , b } ) )
50	49	impcom 446	. . . . . . . 8 |- ( ( E. b b = B /\ -. A e. _V ) -> E. b E. a { A , B } = { a , b } )
51		excom 2042	. . . . . . . 8 |- ( E. a E. b { A , B } = { a , b } <-> E. b E. a { A , B } = { a , b } )
52	50, 51	sylibr 224	. . . . . . 7 |- ( ( E. b b = B /\ -. A e. _V ) -> E. a E. b { A , B } = { a , b } )
53	52	ex 450	. . . . . 6 |- ( E. b b = B -> ( -. A e. _V -> E. a E. b { A , B } = { a , b } ) )
54	53, 5	syl11 33	. . . . 5 |- ( -. A e. _V -> ( B e. _V -> E. a E. b { A , B } = { a , b } ) )
55	32, 54	pm2.61i 176	. . . 4 |- ( B e. _V -> E. a E. b { A , B } = { a , b } )
56	31, 55	jaoi 394	. . 3 |- ( ( A e. _V \/ B e. _V ) -> E. a E. b { A , B } = { a , b } )
57	3, 56	syl 17	. 2 |- ( ( A e. V \/ B e. W ) -> E. a E. b { A , B } = { a , b } )
58		prex 4909	. . 3 |- { A , B } e. _V
59		eqeq1 2626	. . . 4 |- ( p = { A , B } -> ( p = { a , b } <-> { A , B } = { a , b } ) )
60	59	2exbidv 1852	. . 3 |- ( p = { A , B } -> ( E. a E. b p = { a , b } <-> E. a E. b { A , B } = { a , b } ) )
61	58, 60	elab 3350	. 2 |- ( { A , B } e. { p | E. a E. b p = { a , b } } <-> E. a E. b { A , B } = { a , b } )
62	57, 61	sylibr 224	1 |- ( ( A e. V \/ B e. W ) -> { A , B } e. { p | E. a E. b p = { a , b } } )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   _Vcvv 3200   {csn 4177   {cpr 4179

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-nul 3916  df-sn 4178  df-pr 4180

This theorem is referenced by: (None)