Theorem ralopabb

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

	Ref	Expression
Hypotheses	ralopabb.o	$$⊢O=\left\{⟨x,y⟩|\phi \right\}$$
	ralopabb.p	$$⊢o=⟨x,y⟩\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	ralopabb	$$⊢\forall o\in O\psi \leftrightarrow \forall x\forall y\left(\phi \to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ralopabb.o	$$⊢O=\left\{⟨x,y⟩|\phi \right\}$$
2		ralopabb.p	$$⊢o=⟨x,y⟩\to \left(\psi \leftrightarrow \chi \right)$$
3		2nalexn	$$⊢\neg \forall x\forall y\left(\phi \to \chi \right)\leftrightarrow \exists x\exists y\neg \left(\phi \to \chi \right)$$
4	2	notbid	$$⊢o=⟨x,y⟩\to \left(\neg \psi \leftrightarrow \neg \chi \right)$$
5	1 4	rexopabb	$$⊢\exists o\in O\neg \psi \leftrightarrow \exists x\exists y\left(\phi \wedge \neg \chi \right)$$
6		annim	$$⊢\left(\phi \wedge \neg \chi \right)\leftrightarrow \neg \left(\phi \to \chi \right)$$
7	6	2exbii	$$⊢\exists x\exists y\left(\phi \wedge \neg \chi \right)\leftrightarrow \exists x\exists y\neg \left(\phi \to \chi \right)$$
8	5 7	bitri	$$⊢\exists o\in O\neg \psi \leftrightarrow \exists x\exists y\neg \left(\phi \to \chi \right)$$
9		rexnal	$$⊢\exists o\in O\neg \psi \leftrightarrow \neg \forall o\in O\psi$$
10	3 8 9	3bitr2ri	$$⊢\neg \forall o\in O\psi \leftrightarrow \neg \forall x\forall y\left(\phi \to \chi \right)$$
11	10	con4bii	$$⊢\forall o\in O\psi \leftrightarrow \forall x\forall y\left(\phi \to \chi \right)$$