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

Theorem opelxpi 4866
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 4864 . 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 369    e. wcel 1756   <.cop 3878    X. cxp 4833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-opab 4346  df-xp 4841
This theorem is referenced by:  opelvvg  4879  opelvv  4880  opbrop  4911  fliftrel  5996  fnotovb  6124  ov3  6222  ovres  6225  fovrn  6228  fnovrn  6233  ovima0  6237  ovconst2  6238  opabex2  6511  opiota  6628  oprab2co  6653  1stconst  6656  2ndconst  6657  fnwelem  6682  seqomlem2  6898  brdifun  7120  ecopqsi  7149  brecop  7185  eceqoveq  7197  th3q  7201  xpcomco  7393  xpf1o  7465  xpmapenlem  7470  unxpdomlem3  7511  fseqenlem1  8186  fseqenlem2  8187  isfin4-3  8476  axdc4lem  8616  iundom2g  8696  canthp1lem2  8812  addpiord  9045  mulpiord  9046  pinq  9088  nqereu  9090  addpipq  9098  addpqnq  9099  mulpipq  9101  mulpqnq  9102  ordpipq  9103  addpqf  9105  mulpqf  9107  recmulnq  9125  dmrecnq  9129  ltexnq  9136  enreceq  9228  0r  9239  1sr  9240  m1r  9241  addclsr  9242  mulclsr  9243  axaddf  9304  axmulf  9305  xrlenlt  9434  uzrdgfni  11773  swrdval  12305  cnrecnv  12646  ruclem1  13505  ruclem6  13509  eucalgf  13750  eucalg  13754  qredeu  13785  qnumdenbi  13814  crt  13845  phimullem  13846  prmreclem3  13971  setscom  14196  strfv2d  14198  setsid  14207  imasaddfnlem  14458  imasaddflem  14460  imasvscafn  14467  imasvscaval  14468  xpsaddlem  14505  xpsvsca  14509  xpsle  14511  comffval  14630  oppccofval  14647  isoval  14695  funcf2  14770  idfu2nd  14779  resf2nd  14797  wunfunc  14801  funcpropd  14802  fucco  14864  homaval  14891  setcco  14943  catcco  14961  xpcco  14985  xpchom2  14988  xpcco2  14989  xpccatid  14990  prfcl  15005  prf1st  15006  prf2nd  15007  catcxpccl  15009  evlf2  15020  curf1cl  15030  curf2cl  15033  curfcl  15034  uncf1  15038  uncf2  15039  uncfcurf  15041  diag11  15045  diag12  15046  diag2  15047  curf2ndf  15049  hof2fval  15057  yonedalem21  15075  yonedalem22  15080  yonedalem3b  15081  yonffthlem  15084  joindmss  15169  meetdmss  15183  latcl2  15210  latlem  15211  latjcom  15221  latmcom  15237  lsmhash  16193  efgmf  16201  efglem  16204  vrgpf  16256  vrgpinv  16257  frgpuplem  16260  frgpup2  16264  frgpnabllem1  16342  mamudi  18282  mamudir  18283  mamuvs1  18284  mamuvs2  18285  mdetrsca  18385  txbas  19115  txcls  19152  txcnp  19168  upxp  19171  txcnmpt  19172  uptx  19173  txlly  19184  txnlly  19185  txtube  19188  txcmplem1  19189  txlm  19196  lmcn2  19197  tx1stc  19198  txkgen  19200  xkococnlem  19207  cnmpt21  19219  txhmeo  19351  txswaphmeolem  19352  txswaphmeo  19353  ptuncnv  19355  txflf  19554  flfcnp2  19555  tmdcn2  19635  clssubg  19654  divstgplem  19666  tsmsadd  19696  imasdsf1olem  19923  xpsdsval  19931  comet  20063  txmetcnp  20097  metustidOLD  20109  metustid  20110  metustsymOLD  20111  metustsym  20112  nrmmetd  20142  isngp3  20165  ngpds  20170  tngnm  20212  qtopbaslem  20312  cnmetdval  20325  remetdval  20341  tgqioo  20352  cnheiborlem  20501  bndth  20505  htpyco2  20526  phtpyco2  20537  bcthlem5  20814  ovollb2lem  20946  ovolctb  20948  ovoliunlem2  20961  ovolscalem1  20971  ovolicc1  20974  ioombl1lem1  21014  ioorf  21028  ioorcl  21032  dyadf  21046  itg1addlem4  21152  limccnp2  21342  dvcnp2  21369  dvaddbr  21387  dvmulbr  21388  dvcobr  21395  dvef  21427  lhop1lem  21460  taylthlem2  21814  dvdsmulf1o  22509  tgelrnln  23006  tghilbert1_1  23013  brcgr  23097  imsdval  24028  sspval  24072  elovimad  25907  ofoprabco  25933  f1od2  25975  prsdm  26296  prsrn  26297  mbfmco2  26632  eulerpartlemgh  26713  afsval  26947  erdszelem9  27039  cvmlift2lem1  27143  cvmlift2lem9  27152  cvmlift2lem10  27153  cvmlift2lem12  27155  cvmlift2lem13  27156  cvmliftphtlem  27158  fvtransport  28014  colinearex  28042  finixpnum  28367  heicant  28379  mblfinlem1  28381  mblfinlem2  28382  ftc1anc  28428  areacirc  28442  opropabco  28570  heiborlem5  28667  fnotaovb  30057  aovmpt4g  30060  el2xptp0  30080  matsubgcell  30783  matvscacell  30784  pmatcollpw2lem  30820  dvhelvbasei  34573  dvhopvadd  34578  dvhvaddcl  34580  dvhopvsca  34587  dvhvscacl  34588  dvhgrp  34592  dvhopclN  34598  dvhopaddN  34599  dvhopspN  34600  dib1dim2  34653  diblss  34655  diclspsn  34679  dih1dimatlem  34814
  Copyright terms: Public domain W3C validator