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∀zxAy∧xAz→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∀zyA-1x∧xAz→yIz
3 breq1 ⊢y=w→yA-1x↔wA-1x
4 3 anbi1d ⊢y=w→yA-1x∧xAz↔wA-1x∧xAz
5 breq1 ⊢y=w→yIz↔wIz
6 4 5 imbi12d ⊢y=w→yA-1x∧xAz→yIz↔wA-1x∧xAz→wIz
7 6 albidv ⊢y=w→∀zyA-1x∧xAz→yIz↔∀zwA-1x∧xAz→wIz
8 breq2 ⊢x=w→yA-1x↔yA-1w
9 breq1 ⊢x=w→xAz↔wAz
10 8 9 anbi12d ⊢x=w→yA-1x∧xAz↔yA-1w∧wAz
11 10 imbi1d ⊢x=w→yA-1x∧xAz→yIz↔yA-1w∧wAz→yIz
12 11 albidv ⊢x=w→∀zyA-1x∧xAz→yIz↔∀zyA-1w∧wAz→yIz
13 7 12 alcomw ⊢∀y∀x∀zyA-1x∧xAz→yIz↔∀x∀y∀zyA-1x∧xAz→yIz
14 vex ⊢y∈V
15 vex ⊢x∈V
16 14 15 brcnv ⊢yA-1x↔xAy
17 16 anbi1i ⊢yA-1x∧xAz↔xAy∧xAz
18 vex ⊢z∈V
19 18 ideq ⊢yIz↔y=z
20 17 19 imbi12i ⊢yA-1x∧xAz→yIz↔xAy∧xAz→y=z
21 20 3albii ⊢∀x∀y∀zyA-1x∧xAz→yIz↔∀x∀y∀zxAy∧xAz→y=z
22 13 21 bitri ⊢∀y∀x∀zyA-1x∧xAz→yIz↔∀x∀y∀zxAy∧xAz→y=z
23 2 22 bitri ⊢A∘A-1⊆I↔∀x∀y∀zxAy∧xAz→y=z
24 23 anbi2i ⊢Rel⁡A∧A∘A-1⊆I↔Rel⁡A∧∀x∀y∀zxAy∧xAz→y=z
25 1 24 bitri ⊢Fun⁡A↔Rel⁡A∧∀x∀y∀zxAy∧xAz→y=z