Theorem gdlop2fv

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

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

Proof

Step	Hyp	Ref	Expression
1		gdlop2fv.1	$$⊢\phi \to A\in V$$
2		gdlop2fv.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		inex1g	$$⊢A\in V\to A\cap \mathrm{E}\in \mathrm{V}$$
6	1 5	syl	$$⊢\phi \to A\cap \mathrm{E}\in \mathrm{V}$$
7		ineq1	$$⊢A=x\to A\cap \mathrm{E}=x\cap \mathrm{E}$$
8	7	adantl	$$⊢\left(\phi \wedge A=x\right)\to A\cap \mathrm{E}=x\cap \mathrm{E}$$
9		eqidd	$$⊢\left(\phi \wedge B=y\right)\to A\cap \mathrm{E}=A\cap \mathrm{E}$$
10		df-gdlop2	Could not format ~F2 = ( x e. _V , y e. _V |-> ( x i^i _E ) ) : No typesetting found for |- ~F2 = ( x e. _V , y e. _V |-> ( x i^i _E ) ) with typecode |-
11	3 4 6 8 9 10	mpofvop2d	Could not format ( ph -> ( ~F2 ` <. A , B >. ) = ( A i^i _E ) ) : No typesetting found for |- ( ph -> ( ~F2 ` <. A , B >. ) = ( A i^i _E ) ) with typecode |-