Metamath Proof Explorer


Theorem onintss

Description: If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of Suppes p. 228. (Contributed by NM, 3-Oct-2003)

Ref Expression
Hypothesis onintss.1 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
Assertion onintss ( 𝐴 ∈ On → ( 𝜓 { 𝑥 ∈ On ∣ 𝜑 } ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 onintss.1 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
2 1 intminss ( ( 𝐴 ∈ On ∧ 𝜓 ) → { 𝑥 ∈ On ∣ 𝜑 } ⊆ 𝐴 )
3 2 ex ( 𝐴 ∈ On → ( 𝜓 { 𝑥 ∈ On ∣ 𝜑 } ⊆ 𝐴 ) )