This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem epel

Description: The membership relation and the membership predicate agree when the "containing" class is a setvar. Definition 1.6 of Schloeder p. 1. (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 e. x )

Proof

Step	Hyp	Ref	Expression
1		vex	\|- x e. _V
2	1	epeli	\|- ( A _E x <-> A e. x )