Theorem elunirnALT

Description: Alternate proof of elunirn . It is shorter but requires ax-pow (through eluniima , funiunfv , ndmfv ). (Contributed by NM, 24-Sep-2006) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elunirnALT	⊢ ( Fun 𝐹 → ( 𝐴 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		imadmrn	⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹
2	1	unieqi	⊢ ∪ ( 𝐹 “ dom 𝐹 ) = ∪ ran 𝐹
3	2	eleq2i	⊢ ( 𝐴 ∈ ∪ ( 𝐹 “ dom 𝐹 ) ↔ 𝐴 ∈ ∪ ran 𝐹 )
4		eluniima	⊢ ( Fun 𝐹 → ( 𝐴 ∈ ∪ ( 𝐹 “ dom 𝐹 ) ↔ ∃ 𝑥 ∈ dom 𝐹 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )
5	3 4	bitr3id	⊢ ( Fun 𝐹 → ( 𝐴 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )