Theorem ixpsnval

Description: The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018)

	Ref	Expression
Assertion	ixpsnval	$$⊢X\in V\to \underset{x\in \left\{X\right\}}{⨉}B=\left\{f|\left(fFn\left\{X\right\}\wedge f\left(X\right)\in ⦋X/x⦌B\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfixp	$$⊢\underset{x\in \left\{X\right\}}{⨉}B=\left\{f|\left(fFn\left\{X\right\}\wedge \forall x\in \left\{X\right\}f\left(x\right)\in B\right)\right\}$$
2		ralsnsg	$$⊢X\in V\to \left(\forall x\in \left\{X\right\}f\left(x\right)\in B\leftrightarrow \underset{\dot{}}{[}X/x\underset{\dot{}}{]}f\left(x\right)\in B\right)$$
3		sbcel12	$$⊢\underset{\dot{}}{[}X/x\underset{\dot{}}{]}f\left(x\right)\in B\leftrightarrow ⦋X/x⦌f\left(x\right)\in ⦋X/x⦌B$$
4		csbfv2g	$$⊢X\in V\to ⦋X/x⦌f\left(x\right)=f\left(⦋X/x⦌x\right)$$
5		csbvarg	$$⊢X\in V\to ⦋X/x⦌x=X$$
6	5	fveq2d	$$⊢X\in V\to f\left(⦋X/x⦌x\right)=f\left(X\right)$$
7	4 6	eqtrd	$$⊢X\in V\to ⦋X/x⦌f\left(x\right)=f\left(X\right)$$
8	7	eleq1d	$$⊢X\in V\to \left(⦋X/x⦌f\left(x\right)\in ⦋X/x⦌B\leftrightarrow f\left(X\right)\in ⦋X/x⦌B\right)$$
9	3 8	bitrid	$$⊢X\in V\to \left(\underset{\dot{}}{[}X/x\underset{\dot{}}{]}f\left(x\right)\in B\leftrightarrow f\left(X\right)\in ⦋X/x⦌B\right)$$
10	2 9	bitrd	$$⊢X\in V\to \left(\forall x\in \left\{X\right\}f\left(x\right)\in B\leftrightarrow f\left(X\right)\in ⦋X/x⦌B\right)$$
11	10	anbi2d	$$⊢X\in V\to \left(\left(fFn\left\{X\right\}\wedge \forall x\in \left\{X\right\}f\left(x\right)\in B\right)\leftrightarrow \left(fFn\left\{X\right\}\wedge f\left(X\right)\in ⦋X/x⦌B\right)\right)$$
12	11	abbidv	$$⊢X\in V\to \left\{f|\left(fFn\left\{X\right\}\wedge \forall x\in \left\{X\right\}f\left(x\right)\in B\right)\right\}=\left\{f|\left(fFn\left\{X\right\}\wedge f\left(X\right)\in ⦋X/x⦌B\right)\right\}$$
13	1 12	eqtrid	$$⊢X\in V\to \underset{x\in \left\{X\right\}}{⨉}B=\left\{f|\left(fFn\left\{X\right\}\wedge f\left(X\right)\in ⦋X/x⦌B\right)\right\}$$