Metamath Proof Explorer


Theorem elopab

Description: Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998)

Ref Expression
Assertion elopab A x y | φ x y A = x y φ

Proof

Step Hyp Ref Expression
1 elex A x y | φ A V
2 opex x y V
3 eleq1 A = x y A V x y V
4 2 3 mpbiri A = x y A V
5 4 adantr A = x y φ A V
6 5 exlimivv x y A = x y φ A V
7 elopabw A V A x y | φ x y A = x y φ
8 1 6 7 pm5.21nii A x y | φ x y A = x y φ