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

Theorem opelxp 4909
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 4897 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
2 vex 2960 . . . . . . 7  |-  x  e. 
_V
3 vex 2960 . . . . . . 7  |-  y  e. 
_V
42, 3opth2 4439 . . . . . 6  |-  ( <. A ,  B >.  = 
<. x ,  y >.  <->  ( A  =  x  /\  B  =  y )
)
5 eleq1 2497 . . . . . . 7  |-  ( A  =  x  ->  ( A  e.  C  <->  x  e.  C ) )
6 eleq1 2497 . . . . . . 7  |-  ( B  =  y  ->  ( B  e.  D  <->  y  e.  D ) )
75, 6bi2anan9 845 . . . . . 6  |-  ( ( A  =  x  /\  B  =  y )  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
84, 7sylbi 189 . . . . 5  |-  ( <. A ,  B >.  = 
<. x ,  y >.  ->  ( ( A  e.  C  /\  B  e.  D )  <->  ( x  e.  C  /\  y  e.  D ) ) )
98biimprcd 218 . . . 4  |-  ( ( x  e.  C  /\  y  e.  D )  ->  ( <. A ,  B >.  =  <. x ,  y
>.  ->  ( A  e.  C  /\  B  e.  D ) ) )
109rexlimivv 2836 . . 3  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  ->  ( A  e.  C  /\  B  e.  D )
)
11 eqid 2437 . . . 4  |-  <. A ,  B >.  =  <. A ,  B >.
12 opeq1 3985 . . . . . 6  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
1312eqeq2d 2448 . . . . 5  |-  ( x  =  A  ->  ( <. A ,  B >.  = 
<. x ,  y >.  <->  <. A ,  B >.  = 
<. A ,  y >.
) )
14 opeq2 3986 . . . . . 6  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
1514eqeq2d 2448 . . . . 5  |-  ( y  =  B  ->  ( <. A ,  B >.  = 
<. A ,  y >.  <->  <. A ,  B >.  = 
<. A ,  B >. ) )
1613, 15rspc2ev 3061 . . . 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 1269 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  ->  E. x  e.  C  E. y  e.  D  <. A ,  B >.  = 
<. x ,  y >.
)
1810, 17impbii 182 . 2  |-  ( E. x  e.  C  E. y  e.  D  <. A ,  B >.  =  <. x ,  y >.  <->  ( A  e.  C  /\  B  e.  D ) )
191, 18bitri 242 1  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   E.wrex 2707   <.cop 3818    X. cxp 4877
This theorem is referenced by:  brxp  4910  opelxpi  4911  opelxp1  4912  opelxp2  4913  opthprc  4926  elxp3  4929  opeliunxp  4930  optocl  4953  xpsspwOLD  4988  xpiindi  5011  opelres  5152  resiexg  5189  codir  5255  qfto  5256  xpnz  5293  ssrnres  5310  dfco2  5370  relssdmrn  5391  ressn  5409  opelf  5607  oprab4  6144  resoprab  6167  oprssdm  6229  nssdmovg  6230  ndmovg  6231  elmpt2cl  6289  fo1stres  6371  fo2ndres  6372  difxp  6381  dfoprab4  6405  bropopvvv  6427  curry1  6439  curry2  6442  xporderlem  6458  fnwelem  6462  mpt2xopxprcov0  6469  opiota  6536  brecop  6998  brecop2  6999  eceqoveq  7010  xpdom2  7204  mapunen  7277  dfac5lem2  8006  iunfo  8415  ordpipq  8820  opelcn  9005  opelreal  9006  elreal2  9008  swrd00  11766  swrdcl  11767  fsumcom2  12559  phimullem  13169  imasvscafn  13763  homarcl2  14191  evlfcl  14320  iscnp2  17304  txuni2  17598  txcls  17637  txcnpi  17641  txcnp  17653  txcnmpt  17657  txdis1cn  17668  txtube  17673  hausdiag  17678  txlm  17681  tx1stc  17683  txkgen  17685  txflf  18039  tmdcn2  18120  tgphaus  18147  divstgplem  18151  fmucndlem  18322  xmeterval  18463  metustexhalfOLD  18594  metustexhalf  18595  blval2  18606  metuel2  18610  bcthlem1  19278  ovolfcl  19364  ovoliunlem1  19399  ovolshftlem1  19406  mbfimaopnlem  19548  limccnp2  19780  cxpcn3  20633  fsumvma  20998  lgsquadlem1  21139  lgsquadlem2  21140  ofresid  24056  xppreima2  24061  erdszelem10  24887  cvmlift2lem10  25000  cvmlift2lem12  25002  fprodcom2  25309  dfso2  25378  txpss3v  25724  pprodss4v  25730  dfrdg4  25796  heiborlem3  26523  pellex  26899  ndmaovg  28025  aoprssdm  28043  ndmaovcl  28044  ndmaovrcl  28045  ndmaovcom  28046  ndmaovass  28047  ndmaovdistr  28048  el2xptp0  28062  otel3xp  28063  2wlkonot3v  28343  2spthonot3v  28344  2wlkonotv  28345  dibopelvalN  31942  dibopelval2  31944  dib1dim  31964  dihopcl  32052  dih1  32085  dih1dimatlem  32128  hdmap1val  32598
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pr 4404
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-sn 3821  df-pr 3822  df-op 3824  df-opab 4268  df-xp 4885
  Copyright terms: Public domain W3C validator