Theorem dmopabelb

Description: A set is an element of the domain of an 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 -> ( ph <-> ps ) )
Assertion	dmopabelb	|- ( X e. V -> ( X e. dom { <. x , y >. | ph } <-> E. y ps ) )

Proof

Step	Hyp	Ref	Expression
1		dmopabel.d	|- ( x = X -> ( ph <-> ps ) )
2		dmopab	|- dom { <. x , y >. | ph } = { x | E. y ph }
3	2	eleq2i	|- ( X e. dom { <. x , y >. | ph } <-> X e. { x | E. y ph } )
4	1	exbidv	|- ( x = X -> ( E. y ph <-> E. y ps ) )
5		eqid	|- { x | E. y ph } = { x | E. y ph }
6	4 5	elab2g	|- ( X e. V -> ( X e. { x | E. y ph } <-> E. y ps ) )
7	3 6	bitrid	|- ( X e. V -> ( X e. dom { <. x , y >. | ph } <-> E. y ps ) )