Theorem gdlop1fv

Description: The value of the first Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026)

	Ref	Expression
Hypotheses	gdlop1fv.1	|- ( ph -> A e. V )
	gdlop1fv.2	|- ( ph -> B e. W )
Assertion	gdlop1fv	|- ( ph -> ( ~F1 ` <. A , B >. ) = { A , B } )

Proof

Step	Hyp	Ref	Expression
1		gdlop1fv.1	|- ( ph -> A e. V )
2		gdlop1fv.2	|- ( ph -> B e. W )
3	1	elexd	|- ( ph -> A e. _V )
4	2	elexd	|- ( ph -> B e. _V )
5		prex	|- { A , B } e. _V
6	5	a1i	|- ( ph -> { A , B } e. _V )
7		preq1	|- ( A = x -> { A , y } = { x , y } )
8	7	adantl	|- ( ( ph /\ A = x ) -> { A , y } = { x , y } )
9		preq2	|- ( B = y -> { A , B } = { A , y } )
10	9	adantl	|- ( ( ph /\ B = y ) -> { A , B } = { A , y } )
11		df-gdlop1	|- ~F1 = ( x e. _V , y e. _V |-> { x , y } )
12	3 4 6 8 10 11	mpofvop2d	|- ( ph -> ( ~F1 ` <. A , B >. ) = { A , B } )