Description: Ordered pair membership in a class abstraction of ordered pairs. Compare to elopab . (Contributed by Alan Sare, 8-Feb-2014) (Revised by Mario Carneiro, 6-May-2015) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | opelopab4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elopab | ||
2 | vex | ||
3 | vex | ||
4 | 2 3 | opth | |
5 | eqcom | ||
6 | 4 5 | bitr3i | |
7 | 6 | anbi1i | |
8 | 7 | 2exbii | |
9 | 1 8 | bitr4i |