Metamath Proof Explorer

Theorem elfunsALTV3

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

Ref Expression
Assertion elfunsALTV3 ⊢ F ∈ FunsALTV ↔ ∀ u ∀ x ∀ y u F x ∧ u F y → x = y ∧ F ∈ Rels

Proof

Step Hyp Ref Expression
1 elfunsALTV ⊢ F ∈ FunsALTV ↔ ≀ F ∈ CnvRefRels ∧ F ∈ Rels
2 cosselrels ⊢ F ∈ Rels → ≀ F ∈ Rels
3 2 biantrud ⊢ F ∈ Rels → ∀ u ∀ x ∀ y u F x ∧ u F y → x = y ↔ ∀ u ∀ x ∀ y u F x ∧ u F y → x = y ∧ ≀ F ∈ Rels
4 cosselcnvrefrels3 ⊢ ≀ F ∈ CnvRefRels ↔ ∀ u ∀ x ∀ y u F x ∧ u F y → x = y ∧ ≀ F ∈ Rels
5 3 4 syl6rbbr ⊢ F ∈ Rels → ≀ F ∈ CnvRefRels ↔ ∀ u ∀ x ∀ y u F x ∧ u F y → x = y
6 5 pm5.32ri ⊢ ≀ F ∈ CnvRefRels ∧ F ∈ Rels ↔ ∀ u ∀ x ∀ y u F x ∧ u F y → x = y ∧ F ∈ Rels
7 1 6 bitri ⊢ F ∈ FunsALTV ↔ ∀ u ∀ x ∀ y u F x ∧ u F y → x = y ∧ F ∈ Rels