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

Metamath Proof Explorer

Theorem epfrc

Description: A subset of a well-founded class has a minimal element. (Contributed by NM, 17-Feb-2004) (Revised by David Abernethy, 22-Feb-2011)

Ref Expression
Hypothesis epfrc.1 
|- B e. _V
Assertion epfrc 
|- ( ( _E Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )

Proof

Step Hyp Ref Expression
1 epfrc.1 
 |-  B e. _V
2 1 frc 
 |-  ( ( _E Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B { y e. B | y _E x } = (/) )
3 dfin5 
 |-  ( B i^i x ) = { y e. B | y e. x }
4 epel 
 |-  ( y _E x <-> y e. x )
5 4 rabbii 
 |-  { y e. B | y _E x } = { y e. B | y e. x }
6 3 5 eqtr4i 
 |-  ( B i^i x ) = { y e. B | y _E x }
7 6 eqeq1i 
 |-  ( ( B i^i x ) = (/) <-> { y e. B | y _E x } = (/) )
8 7 rexbii 
 |-  ( E. x e. B ( B i^i x ) = (/) <-> E. x e. B { y e. B | y _E x } = (/) )
9 2 8 sylibr 
 |-  ( ( _E Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )