Metamath Proof Explorer

Theorem fundif

Description: A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021)

Ref Expression
Assertion fundif ⊢ Fun ⁡ F → Fun ⁡ F ∖ A

Proof

Step Hyp Ref Expression
1 reldif ⊢ Rel ⁡ F → Rel ⁡ F ∖ A
2 brdif ⊢ x F ∖ A y ↔ x F y ∧ ¬ x A y
3 brdif ⊢ x F ∖ A z ↔ x F z ∧ ¬ x A z
4 pm2.27 ⊢ x F y ∧ x F z → x F y ∧ x F z → y = z → y = z
5 4 ad2ant2r ⊢ x F y ∧ ¬ x A y ∧ x F z ∧ ¬ x A z → x F y ∧ x F z → y = z → y = z
6 2 3 5 syl2anb ⊢ x F ∖ A y ∧ x F ∖ A z → x F y ∧ x F z → y = z → y = z
7 6 com12 ⊢ x F y ∧ x F z → y = z → x F ∖ A y ∧ x F ∖ A z → y = z
8 7 alimi ⊢ ∀ z x F y ∧ x F z → y = z → ∀ z x F ∖ A y ∧ x F ∖ A z → y = z
9 8 2alimi ⊢ ∀ x ∀ y ∀ z x F y ∧ x F z → y = z → ∀ x ∀ y ∀ z x F ∖ A y ∧ x F ∖ A z → y = z
10 1 9 anim12i ⊢ Rel ⁡ F ∧ ∀ x ∀ y ∀ z x F y ∧ x F z → y = z → Rel ⁡ F ∖ A ∧ ∀ x ∀ y ∀ z x F ∖ A y ∧ x F ∖ A z → y = z
11 dffun2 ⊢ Fun ⁡ F ↔ Rel ⁡ F ∧ ∀ x ∀ y ∀ z x F y ∧ x F z → y = z
12 dffun2 ⊢ Fun ⁡ F ∖ A ↔ Rel ⁡ F ∖ A ∧ ∀ x ∀ y ∀ z x F ∖ A y ∧ x F ∖ A z → y = z
13 10 11 12 3imtr4i ⊢ Fun ⁡ F → Fun ⁡ F ∖ A