Theorem elhfOLD

Description: Obsolete version of elhf as of 27-Sep-2026. (Contributed by Scott Fenton, 9-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elhfOLD	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		r111	$$⊢R_1:\mathrm{On}\underset{1-1}{⟶}\mathrm{V}$$
4		f1fun	$$⊢R_1:\mathrm{On}\underset{1-1}{⟶}\mathrm{V}\to \mathrm{Fun}{R}_1$$
5		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)$$
6	3 4 5	mp2b	$$⊢A\in \bigcup R_1\left[\mathrm{\omega }\right]\leftrightarrow \exists x\in \mathrm{\omega }A\in R_1\left(x\right)$$
7	2 6	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 |-