Metamath Proof Explorer

Theorem dffunALTV5

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV5 . (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion dffunALTV5 ⊢ FunALTV F ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ∧ Rel ⁡ F

Proof

Step Hyp Ref Expression
1 dffunALTV2 ⊢ FunALTV F ↔ ≀ F ⊆ I ∧ Rel ⁡ F
2 cossssid5 ⊢ ≀ F ⊆ I ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅
3 2 anbi1i ⊢ ≀ F ⊆ I ∧ Rel ⁡ F ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ∧ Rel ⁡ F
4 1 3 bitri ⊢ FunALTV F ↔ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ∧ Rel ⁡ F