Metamath Proof Explorer

Theorem epel

Description: The membership relation and the membership predicate agree when the "containing" class is a setvar. (Contributed by NM, 13-Aug-1995) Replace the first setvar variable with a class variable. (Revised by BJ, 13-Sep-2022)

Ref Expression
Assertion epel A E x A x


Step Hyp Ref Expression
1 vex x V
2 1 epeli A E x A x