Metamath Proof Explorer

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 ⊢ O = a ∈ A , b ∈ B ⟼ C
elovmpod.x ⊢ φ → X ∈ A
elovmpod.y ⊢ φ → Y ∈ B
elovmpod.d ⊢ φ → D ∈ V
elovmpod.c ⊢ a = X ∧ b = Y → C = D
Assertion elovmpod ⊢ φ → E ∈ X O Y ↔ E ∈ D

Proof

Step Hyp Ref Expression
1 elovmpod.o ⊢ O = a ∈ A , b ∈ B ⟼ C
2 elovmpod.x ⊢ φ → X ∈ A
3 elovmpod.y ⊢ φ → Y ∈ B
4 elovmpod.d ⊢ φ → D ∈ V
5 elovmpod.c ⊢ a = X ∧ b = Y → C = D
6 1 a1i ⊢ φ → O = a ∈ A , b ∈ B ⟼ C
7 5 adantl ⊢ φ ∧ a = X ∧ b = Y → C = D
8 6 7 2 3 4 ovmpod ⊢ φ → X O Y = D
9 8 eleq2d ⊢ φ → E ∈ X O Y ↔ E ∈ D