Theorem elhf

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

	Ref	Expression
Assertion	elhf	|- ( A e. Hf <-> E. x e. _om A e. ( R1 ` x ) )

Proof

Step	Hyp	Ref	Expression
1		df-hf	|- Hf = U. ( R1 " _om )
2	1	eleq2i	|- ( A e. Hf <-> A e. U. ( R1 " _om ) )
3		r111	|- R1 : On -1-1-> _V
4		f1fun	|- ( R1 : On -1-1-> _V -> Fun R1 )
5		eluniima	|- ( Fun R1 -> ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) ) )
6	3 4 5	mp2b	|- ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) )
7	2 6	bitri	|- ( A e. Hf <-> E. x e. _om A e. ( R1 ` x ) )