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

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