Theorem elopabw

Description: Membership in a class abstraction of ordered pairs. Weaker version of elopab with a sethood antecedent, avoiding ax-sep , ax-nul , and ax-pr . Originally a subproof of elopab . (Contributed by SN, 11-Dec-2024)

	Ref	Expression
Assertion	elopabw	$$⊢A\in V\to \left(A\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢z=A\to \left(z=⟨x,y⟩\leftrightarrow A=⟨x,y⟩\right)$$
2	1	anbi1d	$$⊢z=A\to \left(\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(A=⟨x,y⟩\wedge \phi \right)\right)$$
3	2	2exbidv	$$⊢z=A\to \left(\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge \phi \right)\right)$$
4		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
5	3 4	elab2g	$$⊢A\in V\to \left(A\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(A=⟨x,y⟩\wedge \phi \right)\right)$$