MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elmpt2cl Structured version   Unicode version

Theorem elmpt2cl 6401
Description: If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
Hypothesis
Ref Expression
elmpt2cl.f  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
Assertion
Ref Expression
elmpt2cl  |-  ( 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 elmpt2cl
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 elmpt2cl.f . . . . . 6  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
2 df-mpt2 6192 . . . . . 6  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
31, 2eqtri 2479 . . . . 5  |-  F  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
43dmeqi 5136 . . . 4  |-  dom  F  =  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
5 dmoprabss 6269 . . . 4  |-  dom  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }  C_  ( A  X.  B
)
64, 5eqsstri 3481 . . 3  |-  dom  F  C_  ( A  X.  B
)
7 elfvdm 5812 . . . 4  |-  ( X  e.  ( F `  <. S ,  T >. )  ->  <. S ,  T >.  e.  dom  F )
8 df-ov 6190 . . . 4  |-  ( S F T )  =  ( F `  <. S ,  T >. )
97, 8eleq2s 2557 . . 3  |-  ( X  e.  ( S F T )  ->  <. S ,  T >.  e.  dom  F
)
106, 9sseldi 3449 . 2  |-  ( X  e.  ( S F T )  ->  <. S ,  T >.  e.  ( A  X.  B ) )
11 opelxp 4964 . 2  |-  ( <. S ,  T >.  e.  ( A  X.  B
)  <->  ( S  e.  A  /\  T  e.  B ) )
1210, 11sylib 196 1  |-  ( X  e.  ( S F T )  ->  ( S  e.  A  /\  T  e.  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758   <.cop 3978    X. cxp 4933   dom cdm 4935   ` cfv 5513  (class class class)co 6187   {coprab 6188    |-> cmpt2 6189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4508  ax-nul 4516  ax-pow 4565  ax-pr 4626
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-ne 2644  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3067  df-dif 3426  df-un 3428  df-in 3430  df-ss 3437  df-nul 3733  df-if 3887  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4187  df-br 4388  df-opab 4446  df-xp 4941  df-dm 4945  df-iota 5476  df-fv 5521  df-ov 6190  df-oprab 6191  df-mpt2 6192
This theorem is referenced by:  elmpt2cl1  6402  elmpt2cl2  6403  elovmpt2  6404  ixxssixx  11412  funcrcl  14872  natrcl  14959  ismhm  15565  isghm  15846  isga  15908  isslw  16208  isrhm  16914  rimrcl  16917  islmhm  17211  iscn2  18955  elflim2  19650  isfcls  19695  isnmhm  20438  limcrcl  21462  iscvm  27279  elovmpt2rab  30293  elovmpt2rab1  30294  clwlkswlks  30558  clwwlkprop  30568
  Copyright terms: Public domain W3C validator