Metamath Proof Explorer

Theorem dffunsALTV5

Description: Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021)

Ref Expression
Assertion dffunsALTV5 ⊢ FunsALTV = f ∈ Rels | ∀ x ∈ ran ⁡ f ∀ y ∈ ran ⁡ f x = y ∨ x f -1 ∩ y f -1 = ∅

Proof

Step Hyp Ref Expression
1 dffunsALTV4 ⊢ FunsALTV = f ∈ Rels | ∀ u ∃* x u f x
2 ineccnvmo2 ⊢ ∀ x ∈ ran ⁡ f ∀ y ∈ ran ⁡ f x = y ∨ x f -1 ∩ y f -1 = ∅ ↔ ∀ u ∃* x u f x
3 2 rabbii ⊢ f ∈ Rels | ∀ x ∈ ran ⁡ f ∀ y ∈ ran ⁡ f x = y ∨ x f -1 ∩ y f -1 = ∅ = f ∈ Rels | ∀ u ∃* x u f x
4 1 3 eqtr4i ⊢ FunsALTV = f ∈ Rels | ∀ x ∈ ran ⁡ f ∀ y ∈ ran ⁡ f x = y ∨ x f -1 ∩ y f -1 = ∅