Theorem opreu2reu

Description: If there is a unique ordered pair fulfilling a wff, then there is a double restricted unique existential qualification fulfilling a corresponding wff. (Contributed by AV, 25-Jun-2023) (Revised by AV, 2-Jul-2023)

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

Proof

Step	Hyp	Ref	Expression
1		opreu2reurex.a	|- ( p = <. a , b >. -> ( ph <-> ch ) )
2	1	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 ) )
3		2rexreu	|- ( ( 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 )
4	2 3	sylbi	|- ( E! p e. ( A X. B ) ph -> E! a e. A E! b e. B ch )