Theorem zfregfr

Description: The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995)

	Ref	Expression
Assertion	zfregfr	|- _E Fr A

Proof

Step	Hyp	Ref	Expression
1		dfepfr	|- ( _E Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) )
2		vex	|- x e. _V
3		zfreg	|- ( ( x e. _V /\ x =/= (/) ) -> E. y e. x ( y i^i x ) = (/) )
4	2 3	mpan	|- ( x =/= (/) -> E. y e. x ( y i^i x ) = (/) )
5		incom	|- ( y i^i x ) = ( x i^i y )
6	5	eqeq1i	|- ( ( y i^i x ) = (/) <-> ( x i^i y ) = (/) )
7	6	rexbii	|- ( E. y e. x ( y i^i x ) = (/) <-> E. y e. x ( x i^i y ) = (/) )
8	4 7	sylib	|- ( x =/= (/) -> E. y e. x ( x i^i y ) = (/) )
9	8	adantl	|- ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) )
10	1 9	mpgbir	|- _E Fr A