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\mathrm{E}x\leftrightarrow A\in x$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	epeli	$$⊢A\mathrm{E}x\leftrightarrow A\in x$$