Theorem elhf

Description: Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015) Reduce axiom usage and shorten proof. (Revised by BJ, 27-Sep-2026)

	Ref	Expression
Assertion	elhf	Could not format assertion : No typesetting found for |- ( A e. HF <-> E. x e. _om A e. ( R1 ` x ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-hf	Could not format HF = U. ( R1 " _om ) : No typesetting found for |- HF = U. ( R1 " _om ) with typecode |-
2	1	eleq2i	Could not format ( A e. HF <-> A e. U. ( R1 " _om ) ) : No typesetting found for |- ( A e. HF <-> A e. U. ( R1 " _om ) ) with typecode |-
3		r1fun	$$⊢\mathrm{Fun}{R}_1$$
4		eluniima	$$⊢\mathrm{Fun}{R}_1\to \left(A\in \bigcup R_1\left[\mathrm{\omega }\right]\leftrightarrow \exists x\in \mathrm{\omega }A\in R_1\left(x\right)\right)$$
5	3 4	ax-mp	$$⊢A\in \bigcup R_1\left[\mathrm{\omega }\right]\leftrightarrow \exists x\in \mathrm{\omega }A\in R_1\left(x\right)$$
6	2 5	bitri	Could not format ( A e. HF <-> E. x e. _om A e. ( R1 ` x ) ) : No typesetting found for |- ( A e. HF <-> E. x e. _om A e. ( R1 ` x ) ) with typecode |-