Theorem dmopabelb

Description: A set is an element of the domain of a ordered pair class abstraction iff there is a second set so that both sets fulfil the wff of the class abstraction. (Contributed by AV, 19-Oct-2023)

	Ref	Expression
Hypothesis	dmopabel.d	$$⊢x=X\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	dmopabelb	$$⊢X\in V\to \left(X\in \mathrm{dom}\left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists y\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dmopabel.d	$$⊢x=X\to \left(\phi \leftrightarrow \psi \right)$$
2		dmopab	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\phi \right\}=\left\{x|\exists y\phi \right\}$$
3	2	eleq2i	$$⊢X\in \mathrm{dom}\left\{⟨x,y⟩|\phi \right\}\leftrightarrow X\in \left\{x|\exists y\phi \right\}$$
4	1	exbidv	$$⊢x=X\to \left(\exists y\phi \leftrightarrow \exists y\psi \right)$$
5		eqid	$$⊢\left\{x|\exists y\phi \right\}=\left\{x|\exists y\phi \right\}$$
6	4 5	elab2g	$$⊢X\in V\to \left(X\in \left\{x|\exists y\phi \right\}\leftrightarrow \exists y\psi \right)$$
7	3 6	bitrid	$$⊢X\in V\to \left(X\in \mathrm{dom}\left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists y\psi \right)$$