Metamath Proof Explorer

Theorem elovmpo

Description: Utility lemma for two-parameter classes.

EDITORIAL: can simplify isghm , islmhm . (Contributed by Stefan O'Rear, 21-Jan-2015)

Ref Expression
Hypotheses elovmpo.d ⊢ D = a ∈ A , b ∈ B ⟼ C
elovmpo.c ⊢ C ∈ V
elovmpo.e ⊢ a = X ∧ b = Y → C = E
Assertion elovmpo ⊢ F ∈ X D Y ↔ X ∈ A ∧ Y ∈ B ∧ F ∈ E

Proof

Step Hyp Ref Expression
1 elovmpo.d ⊢ D = a ∈ A , b ∈ B ⟼ C
2 elovmpo.c ⊢ C ∈ V
3 elovmpo.e ⊢ a = X ∧ b = Y → C = E
4 1 elmpocl ⊢ F ∈ X D Y → X ∈ A ∧ Y ∈ B
5 2 gen2 ⊢ ∀ a ∀ b C ∈ V
6 3 eleq1d ⊢ a = X ∧ b = Y → C ∈ V ↔ E ∈ V
7 6 spc2gv ⊢ X ∈ A ∧ Y ∈ B → ∀ a ∀ b C ∈ V → E ∈ V
8 5 7 mpi ⊢ X ∈ A ∧ Y ∈ B → E ∈ V
9 3 1 ovmpoga ⊢ X ∈ A ∧ Y ∈ B ∧ E ∈ V → X D Y = E
10 8 9 mpd3an3 ⊢ X ∈ A ∧ Y ∈ B → X D Y = E
11 10 eleq2d ⊢ X ∈ A ∧ Y ∈ B → F ∈ X D Y ↔ F ∈ E
12 4 11 biadanii ⊢ F ∈ X D Y ↔ X ∈ A ∧ Y ∈ B ∧ F ∈ E
13 df-3an ⊢ X ∈ A ∧ Y ∈ B ∧ F ∈ E ↔ X ∈ A ∧ Y ∈ B ∧ F ∈ E
14 12 13 bitr4i ⊢ F ∈ X D Y ↔ X ∈ A ∧ Y ∈ B ∧ F ∈ E