Metamath Proof Explorer


Theorem dffin1-5

Description: Compact quantifier-free version of the standard definition df-fin . (Contributed by Stefan O'Rear, 6-Jan-2015)

Ref Expression
Assertion dffin1-5 Fin = ( ≈ “ ω )

Proof

Step Hyp Ref Expression
1 ensymb ( 𝑥𝑦𝑦𝑥 )
2 1 rexbii ( ∃ 𝑦 ∈ ω 𝑥𝑦 ↔ ∃ 𝑦 ∈ ω 𝑦𝑥 )
3 2 abbii { 𝑥 ∣ ∃ 𝑦 ∈ ω 𝑥𝑦 } = { 𝑥 ∣ ∃ 𝑦 ∈ ω 𝑦𝑥 }
4 df-fin Fin = { 𝑥 ∣ ∃ 𝑦 ∈ ω 𝑥𝑦 }
5 dfima2 ( ≈ “ ω ) = { 𝑥 ∣ ∃ 𝑦 ∈ ω 𝑦𝑥 }
6 3 4 5 3eqtr4i Fin = ( ≈ “ ω )