Theorem gdlop3fv

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

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

Proof

Step	Hyp	Ref	Expression
1		gdlop3fv.1	$$⊢\phi \to A\in V$$
2		gdlop3fv.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	1	difexd	$$⊢\phi \to A\setminus B\in \mathrm{V}$$
6		difeq1	$$⊢A=x\to A\setminus y=x\setminus y$$
7	6	adantl	$$⊢\left(\phi \wedge A=x\right)\to A\setminus y=x\setminus y$$
8		difeq2	$$⊢B=y\to A\setminus B=A\setminus y$$
9	8	adantl	$$⊢\left(\phi \wedge B=y\right)\to A\setminus B=A\setminus y$$
10		df-gdlop3	Could not format ~F3 = ( x e. _V , y e. _V |-> ( x \ y ) ) : No typesetting found for |- ~F3 = ( x e. _V , y e. _V |-> ( x \ y ) ) with typecode |-
11	3 4 5 7 9 10	mpofvop2d	Could not format ( ph -> ( ~F3 ` <. A , B >. ) = ( A \ B ) ) : No typesetting found for |- ( ph -> ( ~F3 ` <. A , B >. ) = ( A \ B ) ) with typecode |-