Metamath Proof Explorer


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 -> ( 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 syl5bb
 |-  ( X e. V -> ( X e. dom { <. x , y >. | ph } <-> E. y ps ) )