Theorem dfixp

Description: Eliminate the expression { x | x e. A } in df-ixp , under the assumption that A and x are disjoint. This way, we can say that x is bound in X_ x e. A B even if it appears free in A . (Contributed by Mario Carneiro, 12-Aug-2016)

	Ref	Expression
Assertion	dfixp	|- X_ x e. A B = { f | ( f Fn A /\ A. x e. A ( f ` x ) e. B ) }

Proof

Step	Hyp	Ref	Expression
1		df-ixp	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
2		abid2	|- { x | x e. A } = A
3	2	fneq2i	|- ( f Fn { x | x e. A } <-> f Fn A )
4	3	anbi1i	|- ( ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) <-> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
5	4	abbii	|- { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) } = { f | ( f Fn A /\ A. x e. A ( f ` x ) e. B ) }
6	1 5	eqtri	|- X_ x e. A B = { f | ( f Fn A /\ A. x e. A ( f ` x ) e. B ) }