This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Functions 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 𝐹 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )