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

Metamath Proof Explorer

Theorem onminesb

Description: If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of Suppes p. 228. (Contributed by NM, 29-Sep-2003)

Ref Expression
Assertion onminesb ⊢ ∃ x ∈ On φ → [˙ ⋂ x ∈ On | φ / x]˙ φ

Proof

Step Hyp Ref Expression
1 rabn0 ⊢ x ∈ On | φ ≠ ∅ ↔ ∃ x ∈ On φ
2 ssrab2 ⊢ x ∈ On | φ ⊆ On
3 onint ⊢ x ∈ On | φ ⊆ On ∧ x ∈ On | φ ≠ ∅ → ⋂ x ∈ On | φ ∈ x ∈ On | φ
4 2 3 mpan ⊢ x ∈ On | φ ≠ ∅ → ⋂ x ∈ On | φ ∈ x ∈ On | φ
5 1 4 sylbir ⊢ ∃ x ∈ On φ → ⋂ x ∈ On | φ ∈ x ∈ On | φ
6 nfcv ⊢ Ⅎ _ x On
7 6 elrabsf ⊢ ⋂ x ∈ On | φ ∈ x ∈ On | φ ↔ ⋂ x ∈ On | φ ∈ On ∧ [˙ ⋂ x ∈ On | φ / x]˙ φ
8 7 simprbi ⊢ ⋂ x ∈ On | φ ∈ x ∈ On | φ → [˙ ⋂ x ∈ On | φ / x]˙ φ
9 5 8 syl ⊢ ∃ x ∈ On φ → [˙ ⋂ x ∈ On | φ / x]˙ φ