Theorem prelspr

Description: An unordered pair of elements of a fixed set V belongs to the set of all unordered pairs over the set V . (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	prelspr	|- ( ( V e. W /\ ( X e. V /\ Y e. V ) ) -> { X , Y } e. ( Pairs ` V ) )

Proof

Step	Hyp	Ref	Expression
1		prelpwi	|- ( ( X e. V /\ Y e. V ) -> { X , Y } e. ~P V )
2		eqidd	|- ( ( X e. V /\ Y e. V ) -> { X , Y } = { X , Y } )
3		preq1	|- ( a = X -> { a , b } = { X , b } )
4	3	eqeq2d	|- ( a = X -> ( { X , Y } = { a , b } <-> { X , Y } = { X , b } ) )
5		preq2	|- ( b = Y -> { X , b } = { X , Y } )
6	5	eqeq2d	|- ( b = Y -> ( { X , Y } = { X , b } <-> { X , Y } = { X , Y } ) )
7	4 6	rspc2ev	|- ( ( X e. V /\ Y e. V /\ { X , Y } = { X , Y } ) -> E. a e. V E. b e. V { X , Y } = { a , b } )
8	2 7	mpd3an3	|- ( ( X e. V /\ Y e. V ) -> E. a e. V E. b e. V { X , Y } = { a , b } )
9	1 8	jca	|- ( ( X e. V /\ Y e. V ) -> ( { X , Y } e. ~P V /\ E. a e. V E. b e. V { X , Y } = { a , b } ) )
10	9	adantl	|- ( ( V e. W /\ ( X e. V /\ Y e. V ) ) -> ( { X , Y } e. ~P V /\ E. a e. V E. b e. V { X , Y } = { a , b } ) )
11		eqeq1	|- ( p = { X , Y } -> ( p = { a , b } <-> { X , Y } = { a , b } ) )
12	11	2rexbidv	|- ( p = { X , Y } -> ( E. a e. V E. b e. V p = { a , b } <-> E. a e. V E. b e. V { X , Y } = { a , b } ) )
13	12	elrab	|- ( { X , Y } e. { p e. ~P V | E. a e. V E. b e. V p = { a , b } } <-> ( { X , Y } e. ~P V /\ E. a e. V E. b e. V { X , Y } = { a , b } ) )
14	10 13	sylibr	|- ( ( V e. W /\ ( X e. V /\ Y e. V ) ) -> { X , Y } e. { p e. ~P V | E. a e. V E. b e. V p = { a , b } } )
15		sprvalpw	|- ( V e. W -> ( Pairs ` V ) = { p e. ~P V | E. a e. V E. b e. V p = { a , b } } )
16	15	adantr	|- ( ( V e. W /\ ( X e. V /\ Y e. V ) ) -> ( Pairs ` V ) = { p e. ~P V | E. a e. V E. b e. V p = { a , b } } )
17	14 16	eleqtrrd	|- ( ( V e. W /\ ( X e. V /\ Y e. V ) ) -> { X , Y } e. ( Pairs ` V ) )