Theorem ralopabb

Description: Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024)

	Ref	Expression
Hypotheses	ralopabb.o	|- O = { <. x , y >. | ph }
	ralopabb.p	|- ( o = <. x , y >. -> ( ps <-> ch ) )
Assertion	ralopabb	|- ( A. o e. O ps <-> A. x A. y ( ph -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		ralopabb.o	|- O = { <. x , y >. | ph }
2		ralopabb.p	|- ( o = <. x , y >. -> ( ps <-> ch ) )
3		2nalexn	|- ( -. A. x A. y ( ph -> ch ) <-> E. x E. y -. ( ph -> ch ) )
4	2	notbid	|- ( o = <. x , y >. -> ( -. ps <-> -. ch ) )
5	1 4	rexopabb	|- ( E. o e. O -. ps <-> E. x E. y ( ph /\ -. ch ) )
6		annim	|- ( ( ph /\ -. ch ) <-> -. ( ph -> ch ) )
7	6	2exbii	|- ( E. x E. y ( ph /\ -. ch ) <-> E. x E. y -. ( ph -> ch ) )
8	5 7	bitri	|- ( E. o e. O -. ps <-> E. x E. y -. ( ph -> ch ) )
9		rexnal	|- ( E. o e. O -. ps <-> -. A. o e. O ps )
10	3 8 9	3bitr2ri	|- ( -. A. o e. O ps <-> -. A. x A. y ( ph -> ch ) )
11	10	con4bii	|- ( A. o e. O ps <-> A. x A. y ( ph -> ch ) )