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 ⊢ ⨉ x ∈ A B = f | f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 df-ixp ⊢ ⨉ x ∈ A B = f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B
2 abid2 ⊢ x | x ∈ A = A
3 2 fneq2i ⊢ f Fn x | x ∈ A ↔ f Fn A
4 3 anbi1i ⊢ f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
5 4 abbii ⊢ f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B = f | f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
6 1 5 eqtri ⊢ ⨉ x ∈ A B = f | f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B