Description: Any member of a hereditarily finite set is itself a hereditarily finite set. (Contributed by Scott Fenton, 16-Jul-2015) Avoid ax-reg , ax-inf2 . (Revised by BTernaryTau, 17-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hfelhf | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ HF ) → 𝐴 ∈ HF ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elhf4 | ⊢ ( 𝐵 ∈ HF ↔ ( 𝐵 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐵 𝑥 ∈ HF ) ) | |
| 2 | 1 | simprbi | ⊢ ( 𝐵 ∈ HF → ∀ 𝑥 ∈ 𝐵 𝑥 ∈ HF ) |
| 3 | eleq1 | ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ HF ↔ 𝐴 ∈ HF ) ) | |
| 4 | 3 | rspcva | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 ∈ HF ) → 𝐴 ∈ HF ) |
| 5 | 2 4 | sylan2 | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ HF ) → 𝐴 ∈ HF ) |