Theorem fvmptex

Description: Express a function F whose value B may not always be a set in terms of another function G for which sethood is guaranteed. (Note that (IB ) is just shorthand for if ( B e. V , B , (/) ) , and it is always a set by fvex .) Note also that these functions are not the same; wherever B ( C ) is not a set, C is not in the domain of F (so it evaluates to the empty set), but C is in the domain of G , and G ( C ) is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013) (Revised by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	fvmptex.1	$$⊢F=\left(x\in A⟼B\right)$$
	fvmptex.2	$$⊢G=\left(x\in A⟼\mathrm{I}\left(B\right)\right)$$
Assertion	fvmptex	$$⊢F\left(C\right)=G\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvmptex.1	$$⊢F=\left(x\in A⟼B\right)$$
2		fvmptex.2	$$⊢G=\left(x\in A⟼\mathrm{I}\left(B\right)\right)$$
3		csbeq1	$$⊢y=C\to ⦋y/x⦌B=⦋C/x⦌B$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
5		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
6		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
7	4 5 6	cbvmpt	$$⊢\left(x\in A⟼B\right)=\left(y\in A⟼⦋y/x⦌B\right)$$
8	1 7	eqtri	$$⊢F=\left(y\in A⟼⦋y/x⦌B\right)$$
9	3 8	fvmpti	$$⊢C\in A\to F\left(C\right)=\mathrm{I}\left(⦋C/x⦌B\right)$$
10	3	fveq2d	$$⊢y=C\to \mathrm{I}\left(⦋y/x⦌B\right)=\mathrm{I}\left(⦋C/x⦌B\right)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}y\mathrm{I}\left(B\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{I}$$
13	12 5	nffv	$$⊢\underset{\_}{Ⅎ}x\mathrm{I}\left(⦋y/x⦌B\right)$$
14	6	fveq2d	$$⊢x=y\to \mathrm{I}\left(B\right)=\mathrm{I}\left(⦋y/x⦌B\right)$$
15	11 13 14	cbvmpt	$$⊢\left(x\in A⟼\mathrm{I}\left(B\right)\right)=\left(y\in A⟼\mathrm{I}\left(⦋y/x⦌B\right)\right)$$
16	2 15	eqtri	$$⊢G=\left(y\in A⟼\mathrm{I}\left(⦋y/x⦌B\right)\right)$$
17		fvex	$$⊢\mathrm{I}\left(⦋C/x⦌B\right)\in \mathrm{V}$$
18	10 16 17	fvmpt	$$⊢C\in A\to G\left(C\right)=\mathrm{I}\left(⦋C/x⦌B\right)$$
19	9 18	eqtr4d	$$⊢C\in A\to F\left(C\right)=G\left(C\right)$$
20	1	dmmptss	$$⊢\mathrm{dom}F\subseteq A$$
21	20	sseli	$$⊢C\in \mathrm{dom}F\to C\in A$$
22		ndmfv	$$⊢\neg C\in \mathrm{dom}F\to F\left(C\right)=\varnothing$$
23	21 22	nsyl5	$$⊢\neg C\in A\to F\left(C\right)=\varnothing$$
24		fvex	$$⊢\mathrm{I}\left(B\right)\in \mathrm{V}$$
25	24 2	dmmpti	$$⊢\mathrm{dom}G=A$$
26	25	eleq2i	$$⊢C\in \mathrm{dom}G\leftrightarrow C\in A$$
27		ndmfv	$$⊢\neg C\in \mathrm{dom}G\to G\left(C\right)=\varnothing$$
28	26 27	sylnbir	$$⊢\neg C\in A\to G\left(C\right)=\varnothing$$
29	23 28	eqtr4d	$$⊢\neg C\in A\to F\left(C\right)=G\left(C\right)$$
30	19 29	pm2.61i	$$⊢F\left(C\right)=G\left(C\right)$$