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 ${⊢}\underset{{x}\in {A}}{⨉}{B}=\left\{{f}|\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}$

Proof

Step Hyp Ref Expression
1 df-ixp ${⊢}\underset{{x}\in {A}}{⨉}{B}=\left\{{f}|\left({f}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}$
2 abid2 ${⊢}\left\{{x}|{x}\in {A}\right\}={A}$
3 2 fneq2i ${⊢}{f}Fn\left\{{x}|{x}\in {A}\right\}↔{f}Fn{A}$
4 3 anbi1i ${⊢}\left({f}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)↔\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$
5 4 abbii ${⊢}\left\{{f}|\left({f}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}=\left\{{f}|\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}$
6 1 5 eqtri ${⊢}\underset{{x}\in {A}}{⨉}{B}=\left\{{f}|\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}$