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 ⊢ Ⅎ _ x A
dffun6f.2 ⊢ Ⅎ _ y A
Assertion dffun6f ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∃* y x A y

Proof

Step Hyp Ref Expression
1 dffun6f.1 ⊢ Ⅎ _ x A
2 dffun6f.2 ⊢ Ⅎ _ y A
3 dffun3 ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ w ∃ u ∀ v w A v → v = u
4 nfcv ⊢ Ⅎ _ y w
5 nfcv ⊢ Ⅎ _ y v
6 4 2 5 nfbr ⊢ Ⅎ y w A v
7 nfv ⊢ Ⅎ v w A y
8 breq2 ⊢ v = y → w A v ↔ w A y
9 6 7 8 cbvmow ⊢ ∃* v w A v ↔ ∃* y w A y
10 9 albii ⊢ ∀ w ∃* v w A v ↔ ∀ w ∃* y w A y
11 df-mo ⊢ ∃* v w A v ↔ ∃ u ∀ v w A v → v = u
12 11 albii ⊢ ∀ w ∃* v w A v ↔ ∀ w ∃ u ∀ v w A v → v = u
13 nfcv ⊢ Ⅎ _ x w
14 nfcv ⊢ Ⅎ _ x y
15 13 1 14 nfbr ⊢ Ⅎ x w A y
16 15 nfmov ⊢ Ⅎ x ∃* y w A y
17 nfv ⊢ Ⅎ w ∃* y x A y
18 breq1 ⊢ w = x → w A y ↔ x A y
19 18 mobidv ⊢ w = x → ∃* y w A y ↔ ∃* y x A y
20 16 17 19 cbvalv1 ⊢ ∀ w ∃* y w A y ↔ ∀ x ∃* y x A y
21 10 12 20 3bitr3ri ⊢ ∀ x ∃* y x A y ↔ ∀ w ∃ u ∀ v w A v → v = u
22 21 anbi2i ⊢ Rel ⁡ A ∧ ∀ x ∃* y x A y ↔ Rel ⁡ A ∧ ∀ w ∃ u ∀ v w A v → v = u
23 3 22 bitr4i ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∃* y x A y