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 cosselcnvrefrels3 ⊢ ≀ F ∈ CnvRefRels ↔ ∀ u ∀ x ∀ y u F x ∧ u F y → x = y ∧ ≀ F ∈ Rels
3 cosselrels ⊢ F ∈ Rels → ≀ F ∈ Rels
4 3 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
5 2 4 bitr4id ⊢ 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