Theorem reu3op

Description: There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 1-Jul-2023)

	Ref	Expression
Hypothesis	reu3op.a	|- ( p = <. a , b >. -> ( ps <-> ch ) )
Assertion	reu3op	|- ( E! p e. ( X X. Y ) ps <-> ( E. a e. X E. b e. Y ch /\ E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )

Proof

Step	Hyp	Ref	Expression
1		reu3op.a	|- ( p = <. a , b >. -> ( ps <-> ch ) )
2		reu3	|- ( E! p e. ( X X. Y ) ps <-> ( E. p e. ( X X. Y ) ps /\ E. q e. ( X X. Y ) A. p e. ( X X. Y ) ( ps -> p = q ) ) )
3	1	rexxp	|- ( E. p e. ( X X. Y ) ps <-> E. a e. X E. b e. Y ch )
4		eqeq2	|- ( q = <. x , y >. -> ( p = q <-> p = <. x , y >. ) )
5	4	imbi2d	|- ( q = <. x , y >. -> ( ( ps -> p = q ) <-> ( ps -> p = <. x , y >. ) ) )
6	5	ralbidv	|- ( q = <. x , y >. -> ( A. p e. ( X X. Y ) ( ps -> p = q ) <-> A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) ) )
7	6	rexxp	|- ( E. q e. ( X X. Y ) A. p e. ( X X. Y ) ( ps -> p = q ) <-> E. x e. X E. y e. Y A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) )
8		eqeq1	|- ( p = <. a , b >. -> ( p = <. x , y >. <-> <. a , b >. = <. x , y >. ) )
9	1 8	imbi12d	|- ( p = <. a , b >. -> ( ( ps -> p = <. x , y >. ) <-> ( ch -> <. a , b >. = <. x , y >. ) ) )
10	9	ralxp	|- ( A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) <-> A. a e. X A. b e. Y ( ch -> <. a , b >. = <. x , y >. ) )
11		eqcom	|- ( <. a , b >. = <. x , y >. <-> <. x , y >. = <. a , b >. )
12	11	a1i	|- ( ( ( x e. X /\ y e. Y ) /\ ( a e. X /\ b e. Y ) ) -> ( <. a , b >. = <. x , y >. <-> <. x , y >. = <. a , b >. ) )
13	12	imbi2d	|- ( ( ( x e. X /\ y e. Y ) /\ ( a e. X /\ b e. Y ) ) -> ( ( ch -> <. a , b >. = <. x , y >. ) <-> ( ch -> <. x , y >. = <. a , b >. ) ) )
14	13	2ralbidva	|- ( ( x e. X /\ y e. Y ) -> ( A. a e. X A. b e. Y ( ch -> <. a , b >. = <. x , y >. ) <-> A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )
15	10 14	syl5bb	|- ( ( x e. X /\ y e. Y ) -> ( A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) <-> A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )
16	15	2rexbiia	|- ( E. x e. X E. y e. Y A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) <-> E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) )
17	7 16	bitri	|- ( E. q e. ( X X. Y ) A. p e. ( X X. Y ) ( ps -> p = q ) <-> E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) )
18	3 17	anbi12i	|- ( ( E. p e. ( X X. Y ) ps /\ E. q e. ( X X. Y ) A. p e. ( X X. Y ) ( ps -> p = q ) ) <-> ( E. a e. X E. b e. Y ch /\ E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )
19	2 18	bitri	|- ( E! p e. ( X X. Y ) ps <-> ( E. a e. X E. b e. Y ch /\ E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )