Metamath Proof Explorer

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 ⁡ F → A ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F A ∈ F ⁡ x

Proof

Step Hyp Ref Expression
1 imadmrn ⊢ F dom ⁡ F = ran ⁡ F
2 1 unieqi ⊢ ⋃ F dom ⁡ F = ⋃ ran ⁡ F
3 2 eleq2i ⊢ A ∈ ⋃ F dom ⁡ F ↔ A ∈ ⋃ ran ⁡ F
4 eluniima ⊢ Fun ⁡ F → A ∈ ⋃ F dom ⁡ F ↔ ∃ x ∈ dom ⁡ F A ∈ F ⁡ x
5 3 4 bitr3id ⊢ Fun ⁡ F → A ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F A ∈ F ⁡ x