Theorem elovmpod

Description: Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015) Variant of elovmpo in deduction form. (Revised by AV, 20-Apr-2025)

	Ref	Expression
Hypotheses	elovmpod.o	⊢ 𝑂 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 )
	elovmpod.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	elovmpod.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	elovmpod.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	elovmpod.c	⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → 𝐶 = 𝐷 )
Assertion	elovmpod	⊢ ( 𝜑 → ( 𝐸 ∈ ( 𝑋 𝑂 𝑌 ) ↔ 𝐸 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		elovmpod.o	⊢ 𝑂 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 )
2		elovmpod.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3		elovmpod.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4		elovmpod.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
5		elovmpod.c	⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → 𝐶 = 𝐷 )
6	1	a1i	⊢ ( 𝜑 → 𝑂 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) )
7	5	adantl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) ) → 𝐶 = 𝐷 )
8	6 7 2 3 4	ovmpod	⊢ ( 𝜑 → ( 𝑋 𝑂 𝑌 ) = 𝐷 )
9	8	eleq2d	⊢ ( 𝜑 → ( 𝐸 ∈ ( 𝑋 𝑂 𝑌 ) ↔ 𝐸 ∈ 𝐷 ) )