Theorem reuprpr

Description: There is a unique proper unordered pair fulfilling a wff iff there are uniquely two different sets fulfilling a corresponding wff. (Contributed by AV, 30-Apr-2023)

	Ref	Expression
Hypotheses	reupr.a	|- ( p = { a , b } -> ( ps <-> ch ) )
	reupr.x	|- ( p = { x , y } -> ( ps <-> th ) )
Assertion	reuprpr	|- ( X e. V -> ( E! p e. ( PrPairs ` X ) ps <-> E. a e. X E. b e. X ( a =/= b /\ ch /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		reupr.a	|- ( p = { a , b } -> ( ps <-> ch ) )
2		reupr.x	|- ( p = { x , y } -> ( ps <-> th ) )
3		prprsprreu	|- ( X e. V -> ( E! p e. ( PrPairs ` X ) ps <-> E! p e. ( Pairs ` X ) ( ( # ` p ) = 2 /\ ps ) ) )
4		fveqeq2	|- ( p = { a , b } -> ( ( # ` p ) = 2 <-> ( # ` { a , b } ) = 2 ) )
5		hashprg	|- ( ( a e. _V /\ b e. _V ) -> ( a =/= b <-> ( # ` { a , b } ) = 2 ) )
6	5	el2v	|- ( a =/= b <-> ( # ` { a , b } ) = 2 )
7	4 6	bitr4di	|- ( p = { a , b } -> ( ( # ` p ) = 2 <-> a =/= b ) )
8	7 1	anbi12d	|- ( p = { a , b } -> ( ( ( # ` p ) = 2 /\ ps ) <-> ( a =/= b /\ ch ) ) )
9		fveqeq2	|- ( p = { x , y } -> ( ( # ` p ) = 2 <-> ( # ` { x , y } ) = 2 ) )
10		hashprg	|- ( ( x e. _V /\ y e. _V ) -> ( x =/= y <-> ( # ` { x , y } ) = 2 ) )
11	10	el2v	|- ( x =/= y <-> ( # ` { x , y } ) = 2 )
12	9 11	bitr4di	|- ( p = { x , y } -> ( ( # ` p ) = 2 <-> x =/= y ) )
13	12 2	anbi12d	|- ( p = { x , y } -> ( ( ( # ` p ) = 2 /\ ps ) <-> ( x =/= y /\ th ) ) )
14	8 13	reupr	|- ( X e. V -> ( E! p e. ( Pairs ` X ) ( ( # ` p ) = 2 /\ ps ) <-> E. a e. X E. b e. X ( ( a =/= b /\ ch ) /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) ) )
15		df-3an	|- ( ( a =/= b /\ ch /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) <-> ( ( a =/= b /\ ch ) /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) )
16	15	bicomi	|- ( ( ( a =/= b /\ ch ) /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) <-> ( a =/= b /\ ch /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) )
17	16	a1i	|- ( X e. V -> ( ( ( a =/= b /\ ch ) /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) <-> ( a =/= b /\ ch /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) ) )
18	17	2rexbidv	|- ( X e. V -> ( E. a e. X E. b e. X ( ( a =/= b /\ ch ) /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) <-> E. a e. X E. b e. X ( a =/= b /\ ch /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) ) )
19	3 14 18	3bitrd	|- ( X e. V -> ( E! p e. ( PrPairs ` X ) ps <-> E. a e. X E. b e. X ( a =/= b /\ ch /\ A. x e. X A. y e. X ( ( x =/= y /\ th ) -> { x , y } = { a , b } ) ) ) )