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

Theorem opelxpi 5020
Description: Ordered pair membership in a Cartesian product (implication). (Contributed by NM, 28-May-1995.)
Assertion
Ref Expression
opelxpi  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )

Proof of Theorem opelxpi
StepHypRef Expression
1 opelxp 5018 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
21biimpri 206 1  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823   <.cop 4022    X. cxp 4986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-opab 4498  df-xp 4994
This theorem is referenced by:  opelvvg  5034  opelvv  5035  opbrop  5068  fliftrel  6181  elovimad  6310  fnotovb  6311  ov3  6412  ovres  6415  fovrn  6418  fnovrn  6423  ovima0  6427  ovconst2  6428  opabex2  6711  el2xptp0  6817  opiota  6832  oprab2co  6858  1stconst  6861  2ndconst  6862  fnwelem  6888  seqomlem2  7108  brdifun  7330  ecopqsi  7360  brecop  7396  eceqoveq  7408  xpcomco  7600  xpf1o  7672  xpmapenlem  7677  unxpdomlem3  7719  fseqenlem1  8396  fseqenlem2  8397  isfin4-3  8686  axdc4lem  8826  iundom2g  8906  canthp1lem2  9020  addpiord  9251  mulpiord  9252  pinq  9294  nqereu  9296  addpipq  9304  addpqnq  9305  mulpipq  9307  mulpqnq  9308  ordpipq  9309  addpqf  9311  mulpqf  9313  recmulnq  9331  dmrecnq  9335  ltexnq  9342  enreceq  9432  addsrpr  9441  mulsrpr  9442  0r  9446  1sr  9447  m1r  9448  addclsr  9449  mulclsr  9450  axaddf  9511  axmulf  9512  xrlenlt  9641  uzrdgfni  12054  swrdval  12636  cnrecnv  13083  ruclem1  14051  ruclem6  14055  eucalgf  14299  eucalg  14303  qredeu  14335  qnumdenbi  14364  crt  14395  phimullem  14396  prmreclem3  14523  setscom  14751  strfv2d  14753  setsid  14762  imasaddfnlem  15020  imasaddflem  15022  imasvscafn  15029  imasvscaval  15030  xpsaddlem  15067  xpsvsca  15071  xpsle  15073  comffval  15190  oppccofval  15207  isoval  15256  funcf2  15359  idfu2nd  15368  resf2nd  15386  wunfunc  15390  funcpropd  15391  fucco  15453  homaval  15512  setcco  15564  catcco  15582  estrcco  15601  xpcco  15654  xpchom2  15657  xpcco2  15658  xpccatid  15659  prfcl  15674  prf1st  15675  prf2nd  15676  catcxpccl  15678  evlf2  15689  curf1cl  15699  curf2cl  15702  curfcl  15703  uncf1  15707  uncf2  15708  uncfcurf  15710  diag11  15714  diag12  15715  diag2  15716  curf2ndf  15718  hof2fval  15726  yonedalem21  15744  yonedalem22  15749  yonedalem3b  15750  yonffthlem  15753  joindmss  15839  meetdmss  15853  latcl2  15880  latlem  15881  latjcom  15891  latmcom  15907  lsmhash  16925  efgmf  16933  efglem  16936  vrgpf  16988  vrgpinv  16989  frgpuplem  16992  frgpup2  16996  frgpnabllem1  17079  mamudi  19075  mamudir  19076  mamuvs1  19077  mamuvs2  19078  matsubgcell  19106  matvscacell  19108  mdetrsca  19275  pmatcoe1fsupp  19372  txbas  20237  txcls  20274  txcnp  20290  upxp  20293  txcnmpt  20294  uptx  20295  txlly  20306  txnlly  20307  txtube  20310  txcmplem1  20311  txlm  20318  lmcn2  20319  tx1stc  20320  txkgen  20322  xkococnlem  20329  cnmpt21  20341  txhmeo  20473  txswaphmeolem  20474  txswaphmeo  20475  ptuncnv  20477  txflf  20676  flfcnp2  20677  tmdcn2  20757  clssubg  20776  qustgplem  20788  tsmsadd  20818  imasdsf1olem  21045  xpsdsval  21053  comet  21185  txmetcnp  21219  metustidOLD  21231  metustid  21232  metustsymOLD  21233  metustsym  21234  nrmmetd  21264  isngp3  21287  ngpds  21292  tngnm  21334  qtopbaslem  21434  cnmetdval  21447  remetdval  21463  tgqioo  21474  cnheiborlem  21623  bndth  21627  htpyco2  21648  phtpyco2  21659  bcthlem5  21936  ovollb2lem  22068  ovolctb  22070  ovoliunlem2  22083  ovolscalem1  22093  ovolicc1  22096  ioombl1lem1  22137  ioorf  22151  ioorcl  22155  dyadf  22169  itg1addlem4  22275  limccnp2  22465  dvcnp2  22492  dvaddbr  22510  dvmulbr  22511  dvcobr  22518  dvef  22550  lhop1lem  22583  taylthlem2  22938  dvdsmulf1o  23671  tgelrnln  24214  brcgr  24408  imsdval  25793  sspval  25837  ofoprabco  27735  f1od2  27781  fimaproj  28074  qtophaus  28077  prsdm  28134  prsrn  28135  mbfmco2  28476  eulerpartlemgh  28584  afsval  28818  erdszelem9  28910  cvmlift2lem1  29014  cvmlift2lem9  29023  cvmlift2lem10  29024  cvmlift2lem12  29026  cvmlift2lem13  29027  cvmliftphtlem  29029  msubco  29158  msubff1  29183  mvhf  29185  msubvrs  29187  fvtransport  29913  colinearex  29941  finixpnum  30281  heicant  30292  mblfinlem1  30294  mblfinlem2  30295  ftc1anc  30341  areacirc  30355  opropabco  30457  heiborlem5  30554  fnotaovb  32525  aovmpt4g  32528  rngccoALTV  33069  ringccoALTV  33132  rhmsubclem2  33168  rhmsubcALTVlem2  33187  dvhelvbasei  37231  dvhopvadd  37236  dvhvaddcl  37238  dvhopvsca  37245  dvhvscacl  37246  dvhgrp  37250  dvhopclN  37256  dvhopaddN  37257  dvhopspN  37258  dib1dim2  37311  diblss  37313  diclspsn  37337  dih1dimatlem  37472
  Copyright terms: Public domain W3C validator