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∈XDY↔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∈XDY→X∈A∧Y∈B
5 2 gen2 ⊢∀a∀bC∈V
6 3 eleq1d ⊢a=X∧b=Y→C∈V↔E∈V
7 6 spc2gv ⊢X∈A∧Y∈B→∀a∀bC∈V→E∈V
8 5 7 mpi ⊢X∈A∧Y∈B→E∈V
9 3 1 ovmpoga ⊢X∈A∧Y∈B∧E∈V→XDY=E
10 8 9 mpd3an3 ⊢X∈A∧Y∈B→XDY=E
11 10 eleq2d ⊢X∈A∧Y∈B→F∈XDY↔F∈E
12 4 11 biadanii ⊢F∈XDY↔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∈XDY↔X∈A∧Y∈B∧F∈E