Metamath Proof Explorer


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