Metamath Proof Explorer

Theorem dffun2

Description: Alternate definition of a function. (Contributed by NM, 29-Dec-1996) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024) Avoid ax-11 . (Revised by BTernaryTau, 29-Dec-2024)

Ref Expression
Assertion dffun2 ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z

Proof

Step Hyp Ref Expression
1 df-fun ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ A ∘ A -1 ⊆ I
2 cotrg ⊢ A ∘ A -1 ⊆ I ↔ ∀ y ∀ x ∀ z y A -1 x ∧ x A z → y I z
3 breq1 ⊢ y = w → y A -1 x ↔ w A -1 x
4 3 anbi1d ⊢ y = w → y A -1 x ∧ x A z ↔ w A -1 x ∧ x A z
5 breq1 ⊢ y = w → y I z ↔ w I z
6 4 5 imbi12d ⊢ y = w → y A -1 x ∧ x A z → y I z ↔ w A -1 x ∧ x A z → w I z
7 6 albidv ⊢ y = w → ∀ z y A -1 x ∧ x A z → y I z ↔ ∀ z w A -1 x ∧ x A z → w I z
8 breq2 ⊢ x = w → y A -1 x ↔ y A -1 w
9 breq1 ⊢ x = w → x A z ↔ w A z
10 8 9 anbi12d ⊢ x = w → y A -1 x ∧ x A z ↔ y A -1 w ∧ w A z
11 10 imbi1d ⊢ x = w → y A -1 x ∧ x A z → y I z ↔ y A -1 w ∧ w A z → y I z
12 11 albidv ⊢ x = w → ∀ z y A -1 x ∧ x A z → y I z ↔ ∀ z y A -1 w ∧ w A z → y I z
13 7 12 alcomw ⊢ ∀ y ∀ x ∀ z y A -1 x ∧ x A z → y I z ↔ ∀ x ∀ y ∀ z y A -1 x ∧ x A z → y I z
14 vex ⊢ y ∈ V
15 vex ⊢ x ∈ V
16 14 15 brcnv ⊢ y A -1 x ↔ x A y
17 16 anbi1i ⊢ y A -1 x ∧ x A z ↔ x A y ∧ x A z
18 vex ⊢ z ∈ V
19 18 ideq ⊢ y I z ↔ y = z
20 17 19 imbi12i ⊢ y A -1 x ∧ x A z → y I z ↔ x A y ∧ x A z → y = z
21 20 3albii ⊢ ∀ x ∀ y ∀ z y A -1 x ∧ x A z → y I z ↔ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
22 13 21 bitri ⊢ ∀ y ∀ x ∀ z y A -1 x ∧ x A z → y I z ↔ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
23 2 22 bitri ⊢ A ∘ A -1 ⊆ I ↔ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
24 23 anbi2i ⊢ Rel ⁡ A ∧ A ∘ A -1 ⊆ I ↔ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
25 1 24 bitri ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z