Theorem bj-gabima

Description: Generalized class abstraction as a direct image.

TODO: improve the support lemmas elimag and fvelima to nonfreeness hypothesis (and for the latter, biconditional). (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Hypotheses	bj-gabima.nf	$$⊢\phi \to \forall x\phi$$
	bj-gabima.nff	$$⊢\phi \to \underset{\_}{Ⅎ}xF$$
	bj-gabima.fun	$$⊢\phi \to \mathrm{Fun}F$$
	bj-gabima.dm	$$⊢\phi \to \left\{x|\psi \right\}\subseteq \mathrm{dom}F$$
Assertion	bj-gabima	$$⊢\phi \to {{F\left(x\right)\left|x\right|\psi }}=F\left[\left\{x|\psi \right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		bj-gabima.nf	$$⊢\phi \to \forall x\phi$$
2		bj-gabima.nff	$$⊢\phi \to \underset{\_}{Ⅎ}xF$$
3		bj-gabima.fun	$$⊢\phi \to \mathrm{Fun}F$$
4		bj-gabima.dm	$$⊢\phi \to \left\{x|\psi \right\}\subseteq \mathrm{dom}F$$
5		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}xy$$
6		vex	$$⊢y\in \mathrm{V}$$
7	6	a1i	$$⊢\phi \to y\in \mathrm{V}$$
8		df-rex	$$⊢\exists z\in \left\{x|\psi \right\}F\left(z\right)=y\leftrightarrow \exists z\left(z\in \left\{x|\psi \right\}\wedge F\left(z\right)=y\right)$$
9	8	a1i	$$⊢\phi \to \left(\exists z\in \left\{x|\psi \right\}F\left(z\right)=y\leftrightarrow \exists z\left(z\in \left\{x|\psi \right\}\wedge F\left(z\right)=y\right)\right)$$
10		eqcom	$$⊢y=F\left(z\right)\leftrightarrow F\left(z\right)=y$$
11		df-clab	$$⊢z\in \left\{x|\psi \right\}\leftrightarrow \left[z/x\right]\psi$$
12	11	bicomi	$$⊢\left[z/x\right]\psi \leftrightarrow z\in \left\{x|\psi \right\}$$
13	10 12	anbi12ci	$$⊢\left(y=F\left(z\right)\wedge \left[z/x\right]\psi \right)\leftrightarrow \left(z\in \left\{x|\psi \right\}\wedge F\left(z\right)=y\right)$$
14	13	exbii	$$⊢\exists z\left(y=F\left(z\right)\wedge \left[z/x\right]\psi \right)\leftrightarrow \exists z\left(z\in \left\{x|\psi \right\}\wedge F\left(z\right)=y\right)$$
15	14	a1i	$$⊢\phi \to \left(\exists z\left(y=F\left(z\right)\wedge \left[z/x\right]\psi \right)\leftrightarrow \exists z\left(z\in \left\{x|\psi \right\}\wedge F\left(z\right)=y\right)\right)$$
16	1	nf5i	$$⊢Ⅎx\phi$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
18	17	a1i	$$⊢\phi \to \underset{\_}{Ⅎ}xy$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
20	19	a1i	$$⊢\phi \to \underset{\_}{Ⅎ}xz$$
21	2 20	nffvd	$$⊢\phi \to \underset{\_}{Ⅎ}xF\left(z\right)$$
22	18 21	nfeqd	$$⊢\phi \to Ⅎxy=F\left(z\right)$$
23		nfs1v	$$⊢Ⅎx\left[z/x\right]\psi$$
24	23	a1i	$$⊢\phi \to Ⅎx\left[z/x\right]\psi$$
25	22 24	nfand	$$⊢\phi \to Ⅎx\left(y=F\left(z\right)\wedge \left[z/x\right]\psi \right)$$
26		fveq2	$$⊢z=x\to F\left(z\right)=F\left(x\right)$$
27	26	eqeq2d	$$⊢z=x\to \left(y=F\left(z\right)\leftrightarrow y=F\left(x\right)\right)$$
28		sbequ12r	$$⊢z=x\to \left(\left[z/x\right]\psi \leftrightarrow \psi \right)$$
29	27 28	anbi12d	$$⊢z=x\to \left(\left(y=F\left(z\right)\wedge \left[z/x\right]\psi \right)\leftrightarrow \left(y=F\left(x\right)\wedge \psi \right)\right)$$
30	29	a1i	$$⊢\phi \to \left(z=x\to \left(\left(y=F\left(z\right)\wedge \left[z/x\right]\psi \right)\leftrightarrow \left(y=F\left(x\right)\wedge \psi \right)\right)\right)$$
31	16 25 30	cbvexdw	$$⊢\phi \to \left(\exists z\left(y=F\left(z\right)\wedge \left[z/x\right]\psi \right)\leftrightarrow \exists x\left(y=F\left(x\right)\wedge \psi \right)\right)$$
32	9 15 31	3bitr2rd	$$⊢\phi \to \left(\exists x\left(y=F\left(x\right)\wedge \psi \right)\leftrightarrow \exists z\in \left\{x|\psi \right\}F\left(z\right)=y\right)$$
33	1 5 7 32	bj-elgab	$$⊢\phi \to \left(y\in {{F\left(x\right)\left|x\right|\psi }}\leftrightarrow \exists z\in \left\{x|\psi \right\}F\left(z\right)=y\right)$$
34	3	funfnd	$$⊢\phi \to FFn\mathrm{dom}F$$
35	34 4	fvelimabd	$$⊢\phi \to \left(y\in F\left[\left\{x|\psi \right\}\right]\leftrightarrow \exists z\in \left\{x|\psi \right\}F\left(z\right)=y\right)$$
36	33 35	bitr4d	$$⊢\phi \to \left(y\in {{F\left(x\right)\left|x\right|\psi }}\leftrightarrow y\in F\left[\left\{x|\psi \right\}\right]\right)$$
37	36	eqrdv	$$⊢\phi \to {{F\left(x\right)\left|x\right|\psi }}=F\left[\left\{x|\psi \right\}\right]$$