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 ) )