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 | ||
opelopabb.yph | |||
opelopabb.xch | |||
opelopabb.ych | |||
opelopabb.is | |||
Assertion | opelopabb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelopabb.xph | ||
2 | opelopabb.yph | ||
3 | opelopabb.xch | ||
4 | opelopabb.ych | ||
5 | opelopabb.is | ||
6 | elopab | ||
7 | 1 2 3 4 5 | copsex2b | |
8 | 6 7 | syl5bb |