Theorem rexopabb

Description: Restricted existential quantification over an ordered-pair class abstraction. (Contributed by AV, 8-Nov-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rexopabb.o	$$⊢O=\left\{⟨x,y⟩|\phi \right\}$$
2		rexopabb.p	$$⊢o=⟨x,y⟩\to \left(\psi \leftrightarrow \chi \right)$$
3	1	rexeqi	$$⊢\exists o\in O\psi \leftrightarrow \exists o\in \left\{⟨x,y⟩|\phi \right\}\psi$$
4		elopab	$$⊢o\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(o=⟨x,y⟩\wedge \phi \right)$$
5		simprr	$$⊢\left(\psi \wedge \left(o=⟨x,y⟩\wedge \phi \right)\right)\to \phi$$
6	2	biimpd	$$⊢o=⟨x,y⟩\to \left(\psi \to \chi \right)$$
7	6	adantr	$$⊢\left(o=⟨x,y⟩\wedge \phi \right)\to \left(\psi \to \chi \right)$$
8	7	impcom	$$⊢\left(\psi \wedge \left(o=⟨x,y⟩\wedge \phi \right)\right)\to \chi$$
9	5 8	jca	$$⊢\left(\psi \wedge \left(o=⟨x,y⟩\wedge \phi \right)\right)\to \left(\phi \wedge \chi \right)$$
10	9	ex	$$⊢\psi \to \left(\left(o=⟨x,y⟩\wedge \phi \right)\to \left(\phi \wedge \chi \right)\right)$$
11	10	2eximdv	$$⊢\psi \to \left(\exists x\exists y\left(o=⟨x,y⟩\wedge \phi \right)\to \exists x\exists y\left(\phi \wedge \chi \right)\right)$$
12	11	impcom	$$⊢\left(\exists x\exists y\left(o=⟨x,y⟩\wedge \phi \right)\wedge \psi \right)\to \exists x\exists y\left(\phi \wedge \chi \right)$$
13	4 12	sylanb	$$⊢\left(o\in \left\{⟨x,y⟩|\phi \right\}\wedge \psi \right)\to \exists x\exists y\left(\phi \wedge \chi \right)$$
14	13	rexlimiva	$$⊢\exists o\in \left\{⟨x,y⟩|\phi \right\}\psi \to \exists x\exists y\left(\phi \wedge \chi \right)$$
15		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\phi \right\}$$
16		nfv	$$⊢Ⅎx\psi$$
17	15 16	nfrexw	$$⊢Ⅎx\exists o\in \left\{⟨x,y⟩|\phi \right\}\psi$$
18		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\phi \right\}$$
19		nfv	$$⊢Ⅎy\psi$$
20	18 19	nfrexw	$$⊢Ⅎy\exists o\in \left\{⟨x,y⟩|\phi \right\}\psi$$
21		opabidw	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$
22		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
23	22 2	sbcie	$$⊢\underset{\dot{}}{[}⟨x,y⟩/o\underset{\dot{}}{]}\psi \leftrightarrow \chi$$
24		rspesbca	$$⊢\left(⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\wedge \underset{\dot{}}{[}⟨x,y⟩/o\underset{\dot{}}{]}\psi \right)\to \exists o\in \left\{⟨x,y⟩|\phi \right\}\psi$$
25	21 23 24	syl2anbr	$$⊢\left(\phi \wedge \chi \right)\to \exists o\in \left\{⟨x,y⟩|\phi \right\}\psi$$
26	20 25	exlimi	$$⊢\exists y\left(\phi \wedge \chi \right)\to \exists o\in \left\{⟨x,y⟩|\phi \right\}\psi$$
27	17 26	exlimi	$$⊢\exists x\exists y\left(\phi \wedge \chi \right)\to \exists o\in \left\{⟨x,y⟩|\phi \right\}\psi$$
28	14 27	impbii	$$⊢\exists o\in \left\{⟨x,y⟩|\phi \right\}\psi \leftrightarrow \exists x\exists y\left(\phi \wedge \chi \right)$$
29	3 28	bitri	$$⊢\exists o\in O\psi \leftrightarrow \exists x\exists y\left(\phi \wedge \chi \right)$$