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

Theorem opelxpi 4884
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 4882 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
21biimpri 211 1  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1897   <.cop 3985    X. cxp 4850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-opab 4475  df-xp 4858
This theorem is referenced by:  opelvvg  4898  opelvv  4899  opbrop  4932  fpr2g  6149  fliftrel  6225  elovimad  6354  fnotovb  6355  ov3  6459  ovres  6462  fovrn  6465  fnovrn  6470  ovima0  6474  ovconst2  6475  opabex2  6757  el2xptp0  6863  opiota  6878  oprab2co  6907  1stconst  6910  2ndconst  6911  fnwelem  6937  seqomlem2  7193  brdifun  7415  ecopqsi  7445  brecop  7481  eceqoveq  7493  xpcomco  7687  xpf1o  7759  xpmapenlem  7764  unxpdomlem3  7803  fseqenlem1  8480  fseqenlem2  8481  isfin4-3  8770  axdc4lem  8910  iundom2g  8990  canthp1lem2  9103  addpiord  9334  mulpiord  9335  pinq  9377  nqereu  9379  addpipq  9387  addpqnq  9388  mulpipq  9390  mulpqnq  9391  ordpipq  9392  addpqf  9394  mulpqf  9396  recmulnq  9414  dmrecnq  9418  ltexnq  9425  enreceq  9515  addsrpr  9524  mulsrpr  9525  0r  9529  1sr  9530  m1r  9531  addclsr  9532  mulclsr  9533  axaddf  9594  axmulf  9595  xrlenlt  9724  uzrdgfni  12203  swrdval  12809  cnrecnv  13276  ruclem1  14331  ruclem6  14335  eucalgf  14590  eucalg  14594  qredeu  14712  qnumdenbi  14741  crt  14774  phimullem  14775  prmreclem3  14910  setscom  15201  strfv2d  15203  setsid  15212  imasaddfnlem  15482  imasaddflem  15484  imasvscafn  15491  imasvscaval  15492  xpsaddlem  15529  xpsvsca  15533  xpsle  15535  comffval  15652  oppccofval  15669  isoval  15718  funcf2  15821  idfu2nd  15830  resf2nd  15848  wunfunc  15852  funcpropd  15853  fucco  15915  homaval  15974  setcco  16026  catcco  16044  estrcco  16063  xpcco  16116  xpchom2  16119  xpcco2  16120  xpccatid  16121  prfcl  16136  prf1st  16137  prf2nd  16138  catcxpccl  16140  evlf2  16151  curf1cl  16161  curf2cl  16164  curfcl  16165  uncf1  16169  uncf2  16170  uncfcurf  16172  diag11  16176  diag12  16177  diag2  16178  curf2ndf  16180  hof2fval  16188  yonedalem21  16206  yonedalem22  16211  yonedalem3b  16212  yonffthlem  16215  joindmss  16301  meetdmss  16315  latcl2  16342  latlem  16343  latjcom  16353  latmcom  16369  lsmhash  17403  efgmf  17411  efglem  17414  vrgpf  17466  vrgpinv  17467  frgpuplem  17470  frgpup2  17474  frgpnabllem1  17557  mamudi  19476  mamudir  19477  mamuvs1  19478  mamuvs2  19479  matsubgcell  19507  matvscacell  19509  mdetrsca  19676  pmatcoe1fsupp  19773  txbas  20630  txcls  20667  txcnp  20683  upxp  20686  txcnmpt  20687  uptx  20688  txlly  20699  txnlly  20700  txtube  20703  txcmplem1  20704  txlm  20711  lmcn2  20712  tx1stc  20713  txkgen  20715  xkococnlem  20722  cnmpt21  20734  txhmeo  20866  txswaphmeolem  20867  txswaphmeo  20868  ptuncnv  20870  txflf  21069  flfcnp2  21070  tmdcn2  21152  clssubg  21171  qustgplem  21183  tsmsadd  21209  imasdsf1olem  21436  xpsdsval  21444  comet  21576  txmetcnp  21610  metustid  21617  metustsym  21618  nrmmetd  21637  isngp3  21660  ngpds  21665  tngnm  21707  qtopbaslem  21827  cnmetdval  21839  remetdval  21855  tgqioo  21866  cnheiborlem  22030  bndth  22034  htpyco2  22058  phtpyco2  22069  bcthlem5  22344  ovollb2lem  22489  ovolctb  22491  ovoliunlem2  22504  ovolscalem1  22514  ovolicc1  22517  ioombl1lem1  22559  ioorf  22573  ioorcl  22577  ioorfOLD  22578  ioorclOLD  22582  dyadf  22597  itg1addlem4  22705  limccnp2  22895  dvcnp2  22922  dvaddbr  22940  dvmulbr  22941  dvcobr  22948  dvef  22980  lhop1lem  23013  taylthlem2  23377  dvdsmulf1o  24171  tgelrnln  24723  brcgr  24978  imsdval  26366  sspval  26410  ofoprabco  28315  f1od2  28357  fimaproj  28708  qtophaus  28711  prsdm  28768  prsrn  28769  mbfmco2  29135  eulerpartlemgh  29259  afsval  29536  erdszelem9  29970  cvmlift2lem1  30073  cvmlift2lem9  30082  cvmlift2lem10  30083  cvmlift2lem12  30085  cvmlift2lem13  30086  cvmliftphtlem  30088  msubco  30217  msubff1  30242  mvhf  30244  msubvrs  30246  fvtransport  30847  colinearex  30875  icoreunrn  31806  relowlpssretop  31811  finixpnum  31974  poimirlem3  31987  poimirlem4  31988  poimirlem15  31999  poimirlem17  32001  poimirlem20  32004  poimirlem25  32009  poimirlem26  32010  poimirlem27  32011  heicant  32019  mblfinlem1  32021  mblfinlem2  32022  ftc1anc  32069  areacirc  32081  opropabco  32094  heiborlem5  32191  dvhelvbasei  34700  dvhopvadd  34705  dvhvaddcl  34707  dvhopvsca  34714  dvhvscacl  34715  dvhgrp  34719  dvhopclN  34725  dvhopaddN  34726  dvhopspN  34727  dib1dim2  34780  diblss  34782  diclspsn  34806  dih1dimatlem  34941  projf1o  37511  hoicvr  38407  hoicvrrex  38415  ovnsubaddlem1  38429  ovnhoilem1  38460  ovnlecvr2  38469  opnvonmbllem1  38491  fnotaovb  38737  aovmpt4g  38740  rngccoALTV  40262  ringccoALTV  40325  rhmsubclem2  40361  rhmsubcALTVlem2  40380
  Copyright terms: Public domain W3C validator