Description: Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | elopab |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex | ||
2 | opex | ||
3 | eleq1 | ||
4 | 2 3 | mpbiri | |
5 | 4 | adantr | |
6 | 5 | exlimivv | |
7 | elopabw | ||
8 | 1 6 7 | pm5.21nii |