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