Theorem gdlop1fv

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

	Ref	Expression
Hypotheses	gdlop1fv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gdlop1fv.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	gdlop1fv	⊢ ( 𝜑 → ( ℱ1 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { 𝐴 , 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		gdlop1fv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		gdlop1fv.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
4	2	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
5		prex	⊢ { 𝐴 , 𝐵 } ∈ V
6	5	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ V )
7		preq1	⊢ ( 𝐴 = 𝑥 → { 𝐴 , 𝑦 } = { 𝑥 , 𝑦 } )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = 𝑥 ) → { 𝐴 , 𝑦 } = { 𝑥 , 𝑦 } )
9		preq2	⊢ ( 𝐵 = 𝑦 → { 𝐴 , 𝐵 } = { 𝐴 , 𝑦 } )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = 𝑦 ) → { 𝐴 , 𝐵 } = { 𝐴 , 𝑦 } )
11		df-gdlop1	⊢ ℱ1 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑥 , 𝑦 } )
12	3 4 6 8 10 11	mpofvop2d	⊢ ( 𝜑 → ( ℱ1 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { 𝐴 , 𝐵 } )