Theorem opreu2reurex

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

	Ref	Expression
Hypothesis	opreu2reurex.a	|- ( p = <. a , b >. -> ( ph <-> ch ) )
Assertion	opreu2reurex	|- ( E! p e. ( A X. B ) ph <-> ( E! a e. A E. b e. B ch /\ E! b e. B E. a e. A ch ) )

Proof

Step	Hyp	Ref	Expression
1		opreu2reurex.a	|- ( p = <. a , b >. -> ( ph <-> ch ) )
2		eqcom	|- ( <. x , y >. = <. a , b >. <-> <. a , b >. = <. x , y >. )
3		vex	|- a e. _V
4		vex	|- b e. _V
5	3 4	opth	|- ( <. a , b >. = <. x , y >. <-> ( a = x /\ b = y ) )
6	2 5	bitri	|- ( <. x , y >. = <. a , b >. <-> ( a = x /\ b = y ) )
7	6	imbi2i	|- ( ( ch -> <. x , y >. = <. a , b >. ) <-> ( ch -> ( a = x /\ b = y ) ) )
8	7	a1i	|- ( ( ( x e. A /\ y e. B ) /\ ( a e. A /\ b e. B ) ) -> ( ( ch -> <. x , y >. = <. a , b >. ) <-> ( ch -> ( a = x /\ b = y ) ) ) )
9	8	2ralbidva	|- ( ( x e. A /\ y e. B ) -> ( A. a e. A A. b e. B ( ch -> <. x , y >. = <. a , b >. ) <-> A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) )
10	9	2rexbiia	|- ( E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> <. x , y >. = <. a , b >. ) <-> E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) )
11	10	anbi2i	|- ( ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> <. x , y >. = <. a , b >. ) ) <-> ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) )
12	1	reu3op	|- ( E! p e. ( A X. B ) ph <-> ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> <. x , y >. = <. a , b >. ) ) )
13		2reu4	|- ( ( E! a e. A E. b e. B ch /\ E! b e. B E. a e. A ch ) <-> ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) )
14	11 12 13	3bitr4i	|- ( E! p e. ( A X. B ) ph <-> ( E! a e. A E. b e. B ch /\ E! b e. B E. a e. A ch ) )