Metamath Proof Explorer


Theorem elhf

Description: Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015)

Ref Expression
Assertion elhf ( 𝐴 ∈ Hf ↔ ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1𝑥 ) )

Proof

Step Hyp Ref Expression
1 df-hf Hf = ( 𝑅1 “ ω )
2 1 eleq2i ( 𝐴 ∈ Hf ↔ 𝐴 ( 𝑅1 “ ω ) )
3 r111 𝑅1 : On –1-1→ V
4 f1fun ( 𝑅1 : On –1-1→ V → Fun 𝑅1 )
5 eluniima ( Fun 𝑅1 → ( 𝐴 ( 𝑅1 “ ω ) ↔ ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1𝑥 ) ) )
6 3 4 5 mp2b ( 𝐴 ( 𝑅1 “ ω ) ↔ ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1𝑥 ) )
7 2 6 bitri ( 𝐴 ∈ Hf ↔ ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1𝑥 ) )