Theorem gdlop1fv

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

	Ref	Expression
Hypotheses	gdlop1fv.1	$$⊢\phi \to A\in V$$
	gdlop1fv.2	$$⊢\phi \to B\in W$$
Assertion	gdlop1fv	Could not format assertion : No typesetting found for |- ( ph -> ( ~F1 ` <. A , B >. ) = { A , B } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		gdlop1fv.1	$$⊢\phi \to A\in V$$
2		gdlop1fv.2	$$⊢\phi \to B\in W$$
3	1	elexd	$$⊢\phi \to A\in \mathrm{V}$$
4	2	elexd	$$⊢\phi \to B\in \mathrm{V}$$
5		prex	$$⊢\left\{A,B\right\}\in \mathrm{V}$$
6	5	a1i	$$⊢\phi \to \left\{A,B\right\}\in \mathrm{V}$$
7		preq1	$$⊢A=x\to \left\{A,y\right\}=\left\{x,y\right\}$$
8	7	adantl	$$⊢\left(\phi \wedge A=x\right)\to \left\{A,y\right\}=\left\{x,y\right\}$$
9		preq2	$$⊢B=y\to \left\{A,B\right\}=\left\{A,y\right\}$$
10	9	adantl	$$⊢\left(\phi \wedge B=y\right)\to \left\{A,B\right\}=\left\{A,y\right\}$$
11		df-gdlop1	Could not format ~F1 = ( x e. _V , y e. _V |-> { x , y } ) : No typesetting found for |- ~F1 = ( x e. _V , y e. _V |-> { x , y } ) with typecode |-
12	3 4 6 8 10 11	mpofvop2d	Could not format ( ph -> ( ~F1 ` <. A , B >. ) = { A , B } ) : No typesetting found for |- ( ph -> ( ~F1 ` <. A , B >. ) = { A , B } ) with typecode |-