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

Metamath Proof Explorer

Theorem tz7.5

Description: A nonempty subclass of an ordinal class has a minimal element. Proposition 7.5 of TakeutiZaring p. 36. (Contributed by NM, 18-Feb-2004) (Revised by David Abernethy, 16-Mar-2011)

Ref Expression
Assertion tz7.5 
|- ( ( Ord A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )

Proof

Step Hyp Ref Expression
1 ordwe 
 |-  ( Ord A -> _E We A )
2 wefrc 
 |-  ( ( _E We A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )
3 1 2 syl3an1 
 |-  ( ( Ord A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )