Metamath Proof Explorer


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 xAB=f|fFnAxAfxB

Proof

Step Hyp Ref Expression
1 df-ixp xAB=f|fFnx|xAxAfxB
2 abid2 x|xA=A
3 2 fneq2i fFnx|xAfFnA
4 3 anbi1i fFnx|xAxAfxBfFnAxAfxB
5 4 abbii f|fFnx|xAxAfxB=f|fFnAxAfxB
6 1 5 eqtri xAB=f|fFnAxAfxB