Theorem elmpocl 6278

Description: If a two-parameter class is inhabited, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)

Hypothesis

Ref	Expression
elmpocl.f	|- F = ( x e. A , y e. B |-> C )

Assertion

Ref	Expression
elmpocl	|- ( X e. ( S F T ) -> ( S e. A /\ T e. B ) )

Distinct variable groups:   x, A, y   x, B, y

Allowed substitution hints:   C( x, y)   S( x, y)   T( x, y)   F( x, y)   X( x, y)

Proof of Theorem elmpocl

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elmpocl.f	. . . . . 6 |- F = ( x e. A , y e. B |-> C )
2		df-mpo 6084	. . . . . 6 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
3	1, 2	eqtri 2259	. . . . 5 |- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
4	3	dmeqi 4980	. . . 4 |- dom F = dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
5		dmoprabss 6164	. . . 4 |- dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } C_ ( A X. B )
6	4, 5	eqsstri 3280	. . 3 |- dom F C_ ( A X. B )
7	1	mpofun 6184	. . . . . 6 |- Fun F
8		funrel 5392	. . . . . 6 |- ( Fun F -> Rel F )
9	7, 8	ax-mp 5	. . . . 5 |- Rel F
10		relelfvdm 5725	. . . . 5 |- ( ( Rel F /\ X e. ( F ` <. S , T >. ) ) -> <. S , T >. e. dom F )
11	9, 10	mpan 428	. . . 4 |- ( X e. ( F ` <. S , T >. ) -> <. S , T >. e. dom F )
12		df-ov 6082	. . . 4 |- ( S F T ) = ( F ` <. S , T >. )
13	11, 12	eleq2s 2333	. . 3 |- ( X e. ( S F T ) -> <. S , T >. e. dom F )
14	6, 13	sselid 3246	. 2 |- ( X e. ( S F T ) -> <. S , T >. e. ( A X. B ) )
15		opelxp 4802	. 2 |- ( <. S , T >. e. ( A X. B ) <-> ( S e. A /\ T e. B ) )
16	14, 15	sylib 122	1 |- ( X e. ( S F T ) -> ( S e. A /\ T e. B ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   <.cop 3711   X. cxp 4770   dom cdm 4772   Rel wrel 4777   Fun wfun 5369   ` cfv 5375  (class class class)co 6079   {coprab 6080   e. cmpo 6081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-iota 5335  df-fun 5377  df-fv 5383  df-ov 6082  df-oprab 6083  df-mpo 6084

This theorem is used by:  elmpocl1  6279  elmpocl2  6280  elovmpo  6282  elovmporab  6283  elovmporab1w  6284  fczsupp0  6493  suppssdc  6494  elpmi  6935  elmapex  6937  pmsspw  6958  ixxssxr  10285  elixx3g  10286  ixxssixx  10287  eliooxr  10312  elfz2  10401  restsspw  13586  ismhm  13751  isghm  14029  isrhm  14448  rimrcl  14450  restrcl  15251  ssrest  15266  iscn2  15284  ishmeo  15388  limcrcl  15742  clwwlknon  16653