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

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 
 |-  ( A. z ( ( x F y /\ x F z ) -> y = z ) -> A. z ( ( x ( F \ A ) y /\ x ( F \ A ) z ) -> y = z ) )
9 8 2alimi 
 |-  ( A. x A. y A. z ( ( x F y /\ x F z ) -> y = z ) -> A. x A. y A. z ( ( x ( F \ A ) y /\ x ( F \ A ) z ) -> y = z ) )
10 1 9 anim12i 
 |-  ( ( Rel F /\ A. x A. y A. z ( ( x F y /\ x F z ) -> y = z ) ) -> ( Rel ( F \ A ) /\ A. x A. y A. z ( ( x ( F \ A ) y /\ x ( F \ A ) z ) -> y = z ) ) )
11 dffun2 
 |-  ( Fun F <-> ( Rel F /\ A. x A. y A. z ( ( x F y /\ x F z ) -> y = z ) ) )
12 dffun2 
 |-  ( Fun ( F \ A ) <-> ( Rel ( F \ A ) /\ A. x A. y A. z ( ( x ( F \ A ) y /\ x ( F \ A ) z ) -> y = z ) ) )
13 10 11 12 3imtr4i 
 |-  ( Fun F -> Fun ( F \ A ) )