Theorem opreuopreu

Description: There is a unique ordered pair fulfilling a wff iff its components fulfil a corresponding wff. (Contributed by AV, 2-Jul-2023)

	Ref	Expression
Hypothesis	opreuopreu.a	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( ps <-> ph ) )
Assertion	opreuopreu	|- ( E! p e. ( A X. B ) ph <-> E! p e. ( A X. B ) E. a E. b ( p = <. a , b >. /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		opreuopreu.a	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( ps <-> ph ) )
2		elxpi	|- ( p e. ( A X. B ) -> E. a E. b ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) )
3		simprl	|- ( ( ph /\ ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) ) -> p = <. a , b >. )
4		vex	|- a e. _V
5		vex	|- b e. _V
6	4 5	op1st	|- ( 1st ` <. a , b >. ) = a
7	6	eqcomi	|- a = ( 1st ` <. a , b >. )
8	4 5	op2nd	|- ( 2nd ` <. a , b >. ) = b
9	8	eqcomi	|- b = ( 2nd ` <. a , b >. )
10	7 9	pm3.2i	|- ( a = ( 1st ` <. a , b >. ) /\ b = ( 2nd ` <. a , b >. ) )
11		fveq2	|- ( p = <. a , b >. -> ( 1st ` p ) = ( 1st ` <. a , b >. ) )
12	11	eqeq2d	|- ( p = <. a , b >. -> ( a = ( 1st ` p ) <-> a = ( 1st ` <. a , b >. ) ) )
13		fveq2	|- ( p = <. a , b >. -> ( 2nd ` p ) = ( 2nd ` <. a , b >. ) )
14	13	eqeq2d	|- ( p = <. a , b >. -> ( b = ( 2nd ` p ) <-> b = ( 2nd ` <. a , b >. ) ) )
15	12 14	anbi12d	|- ( p = <. a , b >. -> ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) <-> ( a = ( 1st ` <. a , b >. ) /\ b = ( 2nd ` <. a , b >. ) ) ) )
16	10 15	mpbiri	|- ( p = <. a , b >. -> ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) )
17	16 1	syl	|- ( p = <. a , b >. -> ( ps <-> ph ) )
18	17	biimprd	|- ( p = <. a , b >. -> ( ph -> ps ) )
19	18	adantr	|- ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( ph -> ps ) )
20	19	impcom	|- ( ( ph /\ ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) ) -> ps )
21	3 20	jca	|- ( ( ph /\ ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) ) -> ( p = <. a , b >. /\ ps ) )
22	21	ex	|- ( ph -> ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( p = <. a , b >. /\ ps ) ) )
23	22	2eximdv	|- ( ph -> ( E. a E. b ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> E. a E. b ( p = <. a , b >. /\ ps ) ) )
24	2 23	syl5com	|- ( p e. ( A X. B ) -> ( ph -> E. a E. b ( p = <. a , b >. /\ ps ) ) )
25	17	biimpa	|- ( ( p = <. a , b >. /\ ps ) -> ph )
26	25	a1i	|- ( p e. ( A X. B ) -> ( ( p = <. a , b >. /\ ps ) -> ph ) )
27	26	exlimdvv	|- ( p e. ( A X. B ) -> ( E. a E. b ( p = <. a , b >. /\ ps ) -> ph ) )
28	24 27	impbid	|- ( p e. ( A X. B ) -> ( ph <-> E. a E. b ( p = <. a , b >. /\ ps ) ) )
29	28	reubiia	|- ( E! p e. ( A X. B ) ph <-> E! p e. ( A X. B ) E. a E. b ( p = <. a , b >. /\ ps ) )