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

Theorem opelxp 4719
Description: Ordered pair membership in a cross product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opelxp  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )

Proof of Theorem opelxp
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp2 4707 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
2 vex 2791 . . . . . . 7  |-  x  e. 
_V
3 vex 2791 . . . . . . 7  |-  y  e. 
_V
42, 3opth2 4248 . . . . . 6  |-  ( <. A ,  B >.  = 
<. x ,  y >.  <->  ( A  =  x  /\  B  =  y )
)
5 eleq1 2343 . . . . . . 7  |-  ( A  =  x  ->  ( A  e.  C  <->  x  e.  C ) )
6 eleq1 2343 . . . . . . 7  |-  ( B  =  y  ->  ( B  e.  D  <->  y  e.  D ) )
75, 6bi2anan9 843 . . . . . 6  |-  ( ( A  =  x  /\  B  =  y )  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
84, 7sylbi 187 . . . . 5  |-  ( <. A ,  B >.  = 
<. x ,  y >.  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
98biimprcd 216 . . . 4  |-  ( ( x  e.  C  /\  y  e.  D )  ->  ( <. A ,  B >.  =  <. x ,  y
>.  ->  ( A  e.  C  /\  B  e.  D ) ) )
109rexlimivv 2672 . . 3  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  ->  ( A  e.  C  /\  B  e.  D )
)
11 eqid 2283 . . . 4  |-  <. A ,  B >.  =  <. A ,  B >.
12 opeq1 3796 . . . . . 6  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
1312eqeq2d 2294 . . . . 5  |-  ( x  =  A  ->  ( <. A ,  B >.  = 
<. x ,  y >.  <->  <. A ,  B >.  = 
<. A ,  y >.
) )
14 opeq2 3797 . . . . . 6  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
1514eqeq2d 2294 . . . . 5  |-  ( y  =  B  ->  ( <. A ,  B >.  = 
<. A ,  y >.  <->  <. A ,  B >.  = 
<. A ,  B >. ) )
1613, 15rspc2ev 2892 . . . 4  |-  ( ( A  e.  C  /\  B  e.  D  /\  <. A ,  B >.  = 
<. A ,  B >. )  ->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
1711, 16mp3an3 1266 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  ->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
1810, 17impbii 180 . 2  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  <->  ( A  e.  C  /\  B  e.  D ) )
191, 18bitri 240 1  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   E.wrex 2544   <.cop 3643    X. cxp 4687
This theorem is referenced by:  brxp  4720  opelxpi  4721  opelxp1  4722  opelxp2  4723  opthprc  4736  elxp3  4739  opeliunxp  4740  optocl  4764  xpsspwOLD  4798  xpiindi  4821  opelres  4960  resiexg  4997  codir  5063  qfto  5064  xpnz  5099  ssrnres  5116  dfco2  5172  relssdmrn  5193  ressn  5211  opelf  5404  oprab4  5917  resoprab  5940  oprssdm  6002  ndmovg  6003  elmpt2cl  6061  fo1stres  6143  fo2ndres  6144  difxp  6153  dfoprab4  6177  curry1  6210  curry2  6213  xporderlem  6226  fnwelem  6230  opiota  6290  brecop  6751  brecop2  6752  eceqoveq  6763  xpdom2  6957  mapunen  7030  dfac5lem2  7751  iunfo  8161  ordpipq  8566  opelcn  8751  opelreal  8752  elreal2  8754  swrd00  11451  swrdcl  11452  fsumcom2  12237  phimullem  12847  imasvscafn  13439  homarcl2  13867  evlfcl  13996  iscnp2  16969  txuni2  17260  txcls  17299  txcnpi  17302  txcnp  17314  txcnmpt  17318  txdis1cn  17329  txtube  17334  hausdiag  17339  txlm  17342  tx1stc  17344  txkgen  17346  txflf  17701  tmdcn2  17772  tgphaus  17799  divstgplem  17803  xmeterval  17978  bcthlem1  18746  ovolfcl  18826  ovoliunlem1  18861  ovolshftlem1  18868  mbfimaopnlem  19010  limccnp2  19242  cxpcn3  20088  fsumvma  20452  lgsquadlem1  20593  lgsquadlem2  20594  xppreima2  23212  erdszelem10  23731  cvmlift2lem10  23843  cvmlift2lem12  23845  dfso2  24111  txpss3v  24418  pprodss4v  24424  dfrdg4  24488  oprabex2gpop  25036  restidsing  25076  limptlimpr2lem1  25574  limptlimpr2lem2  25575  vecaddonto  25659  vecscmonto  25686  heiborlem3  26537  pellex  26920  matrcl  27466  ndmaovg  28044  aoprssdm  28062  ndmaovcl  28063  ndmaovrcl  28064  ndmaovcom  28065  ndmaovass  28066  ndmaovdistr  28067  nssdmovg  28077  mpt2xopxprcov0  28083  dibopelvalN  31333  dibopelval2  31335  dib1dim  31355  dihopcl  31443  dih1  31476  dih1dimatlem  31519  hdmap1val  31989
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695
  Copyright terms: Public domain W3C validator