elhf

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

		Ref	Expression
	Assertion	elhf	$⊢ A \in Hf \leftrightarrow \exists x \in ω A \in R_{1} (x)$

Step	Hyp	Ref	Expression
1		df-hf	$⊢ Hf = ⋃ R_{1} [ω]$
2	1	eleq2i	$⊢ A \in Hf \leftrightarrow A \in ⋃ R_{1} [ω]$
3		r111	$⊢ R_{1} : On \underset{1-1}{⟶} V$
4		f1fun	$⊢ R_{1} : On \underset{1-1}{⟶} V \to Fun R_{1}$
5		eluniima	$⊢ Fun R_{1} \to (A \in ⋃ R_{1} [ω] \leftrightarrow \exists x \in ω A \in R_{1} (x))$
6	3 4 5	mp2b	$⊢ A \in ⋃ R_{1} [ω] \leftrightarrow \exists x \in ω A \in R_{1} (x)$
7	2 6	bitri	$⊢ A \in Hf \leftrightarrow \exists x \in ω A \in R_{1} (x)$

Metamath Proof Explorer