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 ) ) |
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 ) ) |