Description: Membership of an ordered pair in a class abstraction of ordered pairs, biconditional form. (Contributed by BJ, 17-Dec-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opelopabb.xph | |- ( ph -> A. x ph ) |
|
opelopabb.yph | |- ( ph -> A. y ph ) |
||
opelopabb.xch | |- ( ph -> F/ x ch ) |
||
opelopabb.ych | |- ( ph -> F/ y ch ) |
||
opelopabb.is | |- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) ) |
||
Assertion | opelopabb | |- ( ph -> ( <. A , B >. e. { <. x , y >. | ps } <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelopabb.xph | |- ( ph -> A. x ph ) |
|
2 | opelopabb.yph | |- ( ph -> A. y ph ) |
|
3 | opelopabb.xch | |- ( ph -> F/ x ch ) |
|
4 | opelopabb.ych | |- ( ph -> F/ y ch ) |
|
5 | opelopabb.is | |- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) ) |
|
6 | elopab | |- ( <. A , B >. e. { <. x , y >. | ps } <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) ) |
|
7 | 1 2 3 4 5 | copsex2b | |- ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) ) |
8 | 6 7 | syl5bb | |- ( ph -> ( <. A , B >. e. { <. x , y >. | ps } <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) ) |