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	⊢ 𝐷 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 )
	elovmpo.c	⊢ 𝐶 ∈ V
	elovmpo.e	⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → 𝐶 = 𝐸 )
Assertion	elovmpo	⊢ ( 𝐹 ∈ ( 𝑋 𝐷 𝑌 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 ∈ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		elovmpo.d	⊢ 𝐷 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 )
2		elovmpo.c	⊢ 𝐶 ∈ V
3		elovmpo.e	⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → 𝐶 = 𝐸 )
4	1	elmpocl	⊢ ( 𝐹 ∈ ( 𝑋 𝐷 𝑌 ) → ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )
5	2	gen2	⊢ ∀ 𝑎 ∀ 𝑏 𝐶 ∈ V
6	3	eleq1d	⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( 𝐶 ∈ V ↔ 𝐸 ∈ V ) )
7	6	spc2gv	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑎 ∀ 𝑏 𝐶 ∈ V → 𝐸 ∈ V ) )
8	5 7	mpi	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝐸 ∈ V )
9	3 1	ovmpoga	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐸 ∈ V ) → ( 𝑋 𝐷 𝑌 ) = 𝐸 )
10	8 9	mpd3an3	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐷 𝑌 ) = 𝐸 )
11	10	eleq2d	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑋 𝐷 𝑌 ) ↔ 𝐹 ∈ 𝐸 ) )
12	4 11	biadanii	⊢ ( 𝐹 ∈ ( 𝑋 𝐷 𝑌 ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐹 ∈ 𝐸 ) )
13		df-3an	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 ∈ 𝐸 ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐹 ∈ 𝐸 ) )
14	12 13	bitr4i	⊢ ( 𝐹 ∈ ( 𝑋 𝐷 𝑌 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 ∈ 𝐸 ) )