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	|- ( ph -> A. x ph )
	bj-gabima.nff	|- ( ph -> F/_ x F )
	bj-gabima.fun	|- ( ph -> Fun F )
	bj-gabima.dm	|- ( ph -> { x | ps } C_ dom F )
Assertion	bj-gabima	|- ( ph -> {{ ( F ` x ) | x | ps }} = ( F " { x | ps } ) )

Proof

Step	Hyp	Ref	Expression
1		bj-gabima.nf	|- ( ph -> A. x ph )
2		bj-gabima.nff	|- ( ph -> F/_ x F )
3		bj-gabima.fun	|- ( ph -> Fun F )
4		bj-gabima.dm	|- ( ph -> { x | ps } C_ dom F )
5		nfcvd	|- ( ph -> F/_ x y )
6		vex	|- y e. _V
7	6	a1i	|- ( ph -> y e. _V )
8		df-rex	|- ( E. z e. { x | ps } ( F ` z ) = y <-> E. z ( z e. { x | ps } /\ ( F ` z ) = y ) )
9	8	a1i	|- ( ph -> ( E. z e. { x | ps } ( F ` z ) = y <-> E. z ( z e. { x | ps } /\ ( F ` z ) = y ) ) )
10		eqcom	|- ( y = ( F ` z ) <-> ( F ` z ) = y )
11		df-clab	|- ( z e. { x | ps } <-> [ z / x ] ps )
12	11	bicomi	|- ( [ z / x ] ps <-> z e. { x | ps } )
13	10 12	anbi12ci	|- ( ( y = ( F ` z ) /\ [ z / x ] ps ) <-> ( z e. { x | ps } /\ ( F ` z ) = y ) )
14	13	exbii	|- ( E. z ( y = ( F ` z ) /\ [ z / x ] ps ) <-> E. z ( z e. { x | ps } /\ ( F ` z ) = y ) )
15	14	a1i	|- ( ph -> ( E. z ( y = ( F ` z ) /\ [ z / x ] ps ) <-> E. z ( z e. { x | ps } /\ ( F ` z ) = y ) ) )
16	1	nf5i	|- F/ x ph
17		nfcv	|- F/_ x y
18	17	a1i	|- ( ph -> F/_ x y )
19		nfcv	|- F/_ x z
20	19	a1i	|- ( ph -> F/_ x z )
21	2 20	nffvd	|- ( ph -> F/_ x ( F ` z ) )
22	18 21	nfeqd	|- ( ph -> F/ x y = ( F ` z ) )
23		nfs1v	|- F/ x [ z / x ] ps
24	23	a1i	|- ( ph -> F/ x [ z / x ] ps )
25	22 24	nfand	|- ( ph -> F/ x ( y = ( F ` z ) /\ [ z / x ] ps ) )
26		fveq2	|- ( z = x -> ( F ` z ) = ( F ` x ) )
27	26	eqeq2d	|- ( z = x -> ( y = ( F ` z ) <-> y = ( F ` x ) ) )
28		sbequ12r	|- ( z = x -> ( [ z / x ] ps <-> ps ) )
29	27 28	anbi12d	|- ( z = x -> ( ( y = ( F ` z ) /\ [ z / x ] ps ) <-> ( y = ( F ` x ) /\ ps ) ) )
30	29	a1i	|- ( ph -> ( z = x -> ( ( y = ( F ` z ) /\ [ z / x ] ps ) <-> ( y = ( F ` x ) /\ ps ) ) ) )
31	16 25 30	cbvexdw	|- ( ph -> ( E. z ( y = ( F ` z ) /\ [ z / x ] ps ) <-> E. x ( y = ( F ` x ) /\ ps ) ) )
32	9 15 31	3bitr2rd	|- ( ph -> ( E. x ( y = ( F ` x ) /\ ps ) <-> E. z e. { x | ps } ( F ` z ) = y ) )
33	1 5 7 32	bj-elgab	|- ( ph -> ( y e. {{ ( F ` x ) | x | ps }} <-> E. z e. { x | ps } ( F ` z ) = y ) )
34	3	funfnd	|- ( ph -> F Fn dom F )
35	34 4	fvelimabd	|- ( ph -> ( y e. ( F " { x | ps } ) <-> E. z e. { x | ps } ( F ` z ) = y ) )
36	33 35	bitr4d	|- ( ph -> ( y e. {{ ( F ` x ) | x | ps }} <-> y e. ( F " { x | ps } ) ) )
37	36	eqrdv	|- ( ph -> {{ ( F ` x ) | x | ps }} = ( F " { x | ps } ) )