Metamath Proof Explorer


Theorem dffun3f

Description: Alternate definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Emmett Weisz, 14-Mar-2021)

Ref Expression
Hypotheses dffun3f.1 𝑥 𝐴
dffun3f.2 𝑦 𝐴
dffun3f.3 𝑧 𝐴
Assertion dffun3f ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥𝑧𝑦 ( 𝑥 𝐴 𝑦𝑦 = 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 dffun3f.1 𝑥 𝐴
2 dffun3f.2 𝑦 𝐴
3 dffun3f.3 𝑧 𝐴
4 1 2 dffun6f ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
5 nfcv 𝑧 𝑥
6 nfcv 𝑧 𝑦
7 5 3 6 nfbr 𝑧 𝑥 𝐴 𝑦
8 7 mof ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃ 𝑧𝑦 ( 𝑥 𝐴 𝑦𝑦 = 𝑧 ) )
9 8 albii ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥𝑧𝑦 ( 𝑥 𝐴 𝑦𝑦 = 𝑧 ) )
10 9 anbi2i ( ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥𝑧𝑦 ( 𝑥 𝐴 𝑦𝑦 = 𝑧 ) ) )
11 4 10 bitri ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥𝑧𝑦 ( 𝑥 𝐴 𝑦𝑦 = 𝑧 ) ) )