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 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }

Proof

Step	Hyp	Ref	Expression
1		df-ixp	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }
2		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 } = 𝐴
3	2	fneq2i	⊢ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ↔ 𝑓 Fn 𝐴 )
4	3	anbi1i	⊢ ( ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
5	4	abbii	⊢ { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) } = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }
6	1 5	eqtri	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }