Theorem sprid

Description: Two identical representations of the class of all unordered pairs. (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	sprid	|- { p | E. a e. _V E. b e. _V p = { a , b } } = { p | E. a E. b p = { a , b } }

Proof

Step	Hyp	Ref	Expression
1		rexv	|- ( E. a e. _V E. b e. _V p = { a , b } <-> E. a E. b e. _V p = { a , b } )
2		rexv	|- ( E. b e. _V p = { a , b } <-> E. b p = { a , b } )
3	2	exbii	|- ( E. a E. b e. _V p = { a , b } <-> E. a E. b p = { a , b } )
4	1 3	bitri	|- ( E. a e. _V E. b e. _V p = { a , b } <-> E. a E. b p = { a , b } )
5	4	abbii	|- { p | E. a e. _V E. b e. _V p = { a , b } } = { p | E. a E. b p = { a , b } }