This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dffun6f

Description: Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses dffun6f.1 ⊢ Ⅎ 𝑥 𝐴
dffun6f.2 ⊢ Ⅎ 𝑦 𝐴
Assertion dffun6f ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )

Proof

Step Hyp Ref Expression
1 dffun6f.1 ⊢ Ⅎ 𝑥 𝐴
2 dffun6f.2 ⊢ Ⅎ 𝑦 𝐴
3 dffun3 ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑤 ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) ) )
4 nfcv ⊢ Ⅎ 𝑦 𝑤
5 nfcv ⊢ Ⅎ 𝑦 𝑣
6 4 2 5 nfbr ⊢ Ⅎ 𝑦 𝑤 𝐴 𝑣
7 nfv ⊢ Ⅎ 𝑣 𝑤 𝐴 𝑦
8 breq2 ⊢ ( 𝑣 = 𝑦 → ( 𝑤 𝐴 𝑣 ↔ 𝑤 𝐴 𝑦 ) )
9 6 7 8 cbvmow ⊢ ( ∃* 𝑣 𝑤 𝐴 𝑣 ↔ ∃* 𝑦 𝑤 𝐴 𝑦 )
10 9 albii ⊢ ( ∀ 𝑤 ∃* 𝑣 𝑤 𝐴 𝑣 ↔ ∀ 𝑤 ∃* 𝑦 𝑤 𝐴 𝑦 )
11 df-mo ⊢ ( ∃* 𝑣 𝑤 𝐴 𝑣 ↔ ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) )
12 11 albii ⊢ ( ∀ 𝑤 ∃* 𝑣 𝑤 𝐴 𝑣 ↔ ∀ 𝑤 ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) )
13 nfcv ⊢ Ⅎ 𝑥 𝑤
14 nfcv ⊢ Ⅎ 𝑥 𝑦
15 13 1 14 nfbr ⊢ Ⅎ 𝑥 𝑤 𝐴 𝑦
16 15 nfmov ⊢ Ⅎ 𝑥 ∃* 𝑦 𝑤 𝐴 𝑦
17 nfv ⊢ Ⅎ 𝑤 ∃* 𝑦 𝑥 𝐴 𝑦
18 breq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝐴 𝑦 ↔ 𝑥 𝐴 𝑦 ) )
19 18 mobidv ⊢ ( 𝑤 = 𝑥 → ( ∃* 𝑦 𝑤 𝐴 𝑦 ↔ ∃* 𝑦 𝑥 𝐴 𝑦 ) )
20 16 17 19 cbvalv1 ⊢ ( ∀ 𝑤 ∃* 𝑦 𝑤 𝐴 𝑦 ↔ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 )
21 10 12 20 3bitr3ri ⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑤 ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) )
22 21 anbi2i ⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑤 ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) ) )
23 3 22 bitr4i ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )