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

Theorem opelxp 4735
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 4723 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
2 vex 2804 . . . . . . 7  |-  x  e. 
_V
3 vex 2804 . . . . . . 7  |-  y  e. 
_V
42, 3opth2 4264 . . . . . 6  |-  ( <. A ,  B >.  = 
<. x ,  y >.  <->  ( A  =  x  /\  B  =  y )
)
5 eleq1 2356 . . . . . . 7  |-  ( A  =  x  ->  ( A  e.  C  <->  x  e.  C ) )
6 eleq1 2356 . . . . . . 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 2685 . . 3  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  ->  ( A  e.  C  /\  B  e.  D )
)
11 eqid 2296 . . . 4  |-  <. A ,  B >.  =  <. A ,  B >.
12 opeq1 3812 . . . . . 6  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
1312eqeq2d 2307 . . . . 5  |-  ( x  =  A  ->  ( <. A ,  B >.  = 
<. x ,  y >.  <->  <. A ,  B >.  = 
<. A ,  y >.
) )
14 opeq2 3813 . . . . . 6  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
1514eqeq2d 2307 . . . . 5  |-  ( y  =  B  ->  ( <. A ,  B >.  = 
<. A ,  y >.  <->  <. A ,  B >.  = 
<. A ,  B >. ) )
1613, 15rspc2ev 2905 . . . 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 1632    e. wcel 1696   E.wrex 2557   <.cop 3656    X. cxp 4703
This theorem is referenced by:  brxp  4736  opelxpi  4737  opelxp1  4738  opelxp2  4739  opthprc  4752  elxp3  4755  opeliunxp  4756  optocl  4780  xpsspwOLD  4814  xpiindi  4837  opelres  4976  resiexg  5013  codir  5079  qfto  5080  xpnz  5115  ssrnres  5132  dfco2  5188  relssdmrn  5209  ressn  5227  opelf  5420  oprab4  5933  resoprab  5956  oprssdm  6018  ndmovg  6019  elmpt2cl  6077  fo1stres  6159  fo2ndres  6160  difxp  6169  dfoprab4  6193  curry1  6226  curry2  6229  xporderlem  6242  fnwelem  6246  opiota  6306  brecop  6767  brecop2  6768  eceqoveq  6779  xpdom2  6973  mapunen  7046  dfac5lem2  7767  iunfo  8177  ordpipq  8582  opelcn  8767  opelreal  8768  elreal2  8770  swrd00  11467  swrdcl  11468  fsumcom2  12253  phimullem  12863  imasvscafn  13455  homarcl2  13883  evlfcl  14012  iscnp2  16985  txuni2  17276  txcls  17315  txcnpi  17318  txcnp  17330  txcnmpt  17334  txdis1cn  17345  txtube  17350  hausdiag  17355  txlm  17358  tx1stc  17360  txkgen  17362  txflf  17717  tmdcn2  17788  tgphaus  17815  divstgplem  17819  xmeterval  17994  bcthlem1  18762  ovolfcl  18842  ovoliunlem1  18877  ovolshftlem1  18884  mbfimaopnlem  19026  limccnp2  19258  cxpcn3  20104  fsumvma  20468  lgsquadlem1  20609  lgsquadlem2  20610  xppreima2  23227  erdszelem10  23746  cvmlift2lem10  23858  cvmlift2lem12  23860  dfso2  24182  txpss3v  24489  pprodss4v  24495  dfrdg4  24560  oprabex2gpop  25139  restidsing  25179  limptlimpr2lem1  25677  limptlimpr2lem2  25678  vecaddonto  25762  vecscmonto  25789  heiborlem3  26640  pellex  27023  matrcl  27569  ndmaovg  28152  aoprssdm  28170  ndmaovcl  28171  ndmaovrcl  28172  ndmaovcom  28173  ndmaovass  28174  ndmaovdistr  28175  nssdmovg  28194  mpt2xopxprcov0  28199  trlonprop  28341  dibopelvalN  31955  dibopelval2  31957  dib1dim  31977  dihopcl  32065  dih1  32098  dih1dimatlem  32141  hdmap1val  32611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-opab 4094  df-xp 4711
  Copyright terms: Public domain W3C validator