Metamath Proof Explorer


Theorem opelopab4

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 u v x y | φ x y x = u y = v φ

Proof

Step Hyp Ref Expression
1 elopab u v x y | φ x y u v = x y φ
2 vex x V
3 vex y V
4 2 3 opth x y = u v x = u y = v
5 eqcom x y = u v u v = x y
6 4 5 bitr3i x = u y = v u v = x y
7 6 anbi1i x = u y = v φ u v = x y φ
8 7 2exbii x y x = u y = v φ x y u v = x y φ
9 1 8 bitr4i u v x y | φ x y x = u y = v φ