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

Theorem opelxpi 5627
Description: Ordered pair membership in a Cartesian product (implication). (Contributed by NM, 28-May-1995.)
Assertion
Ref Expression
opelxpi ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpi
StepHypRef Expression
1 opelxp 5626 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 227 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  cop 4568   × cxp 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5138  df-xp 5596
This theorem is referenced by:  opelxpd  5628  opelvv  5629  opelvvg  5630  opbrop  5685  elsnxp  6198  reuop  6200  fnbrfvb2  6835  ov3  7444  ovres  7447  fovrn  7451  fnovrn  7456  ovima0  7460  ovconst2  7461  el2xptp0  7887  opiota  7908  fimaproj  7985  seqomlem2  8291  brdifun  8536  ecopqsi  8572  brecop  8608  eceqoveq  8620  xpcomco  8858  djulcl  9677  djurcl  9678  djulf1o  9679  djurf1o  9680  djuun  9693  isfin4p1  10080  axdc4lem  10220  canthp1lem2  10418  addpiord  10649  mulpiord  10650  pinq  10692  nqereu  10694  addpipq  10702  addpqnq  10703  mulpipq  10705  mulpqnq  10706  ordpipq  10707  recmulnq  10729  dmrecnq  10733  enreceq  10831  addsrpr  10840  mulsrpr  10841  0r  10845  1sr  10846  m1r  10847  addclsr  10848  mulclsr  10849  axaddf  10910  xrlenlt  11049  uzrdgfni  13687  swrdval  14365  ruclem6  15953  eucalgf  16297  eucalg  16301  qnumdenbi  16457  setscom  16890  strfv2d  16912  setsid  16918  imasaddfnlem  17248  imasaddflem  17250  imasvscafn  17257  imasvscaval  17258  funcpropd  17625  fucco  17689  catcxpccl  17933  catcxpcclOLD  17934  curf1cl  17955  curf2cl  17958  curfcl  17959  uncfcurf  17966  diag2  17972  curf2ndf  17974  joindmss  18106  meetdmss  18120  latlem  18164  latjcom  18174  latmcom  18190  efgmf  19328  efglem  19331  vrgpf  19383  vrgpinv  19384  frgpuplem  19387  frgpup2  19391  frgpnabllem1  19483  gsumxp2  19590  mamudi  21559  mamudir  21560  mamuvs1  21561  mamuvs2  21562  matsubgcell  21592  matvscacell  21594  pmatcoe1fsupp  21859  txbas  22727  txcls  22764  upxp  22783  uptx  22785  txtube  22800  txcmplem1  22801  txlm  22808  tx1stc  22810  txkgen  22812  cnmpt21  22831  txswaphmeolem  22964  txswaphmeo  22965  clssubg  23269  qustgplem  23281  comet  23678  txmetcnp  23712  metustsym  23720  nrmmetd  23739  isngp3  23763  ngpds  23769  qtopbaslem  23931  cnmetdval  23943  remetdval  23961  tgqioo  23972  bndth  24130  htpyco2  24151  phtpyco2  24162  ovolicc1  24689  ioorf  24746  ioorcl  24750  itg1addlem4  24872  itg1addlem4OLD  24873  dvcnp2  25093  dvef  25153  lhop1lem  25186  taylthlem2  25542  addsqnreup  26600  brcgr  27277  ex-fpar  28835  imsdval  29057  sspval  29094  opreu2reuALT  30834  2ndimaxp  30993  ofoprabco  31010  f1od2  31065  qtophaus  31795  mbfmco2  32241  eulerpartlemgh  32354  afsval  32660  erdszelem9  33170  cvmlift2lem1  33273  cvmlift2lem9  33282  cvmlift2lem12  33285  cvmlift2lem13  33286  cvmliftphtlem  33288  goel  33318  goelel3xp  33319  sat1el2xp  33350  fmla0xp  33354  prv1n  33402  msubco  33502  msubff1  33527  mvhf  33529  msubvrs  33531  xpord2pred  33801  fvtransport  34343  colinearex  34371  bj-idres  35340  icoreunrn  35539  relowlpssretop  35544  curf  35764  finixpnum  35771  poimirlem15  35801  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  heicant  35821  mblfinlem1  35823  mblfinlem2  35824  ftc1anc  35867  opropabco  35891  heiborlem5  35982  dvhelvbasei  39109  dvhopvadd  39114  dvhvaddcl  39116  dvhopvsca  39123  dvhvscacl  39124  dvhgrp  39128  dvhopclN  39134  dvhopaddN  39135  dvhopspN  39136  dib1dim2  39189  diblss  39191  diclspsn  39215  dih1dimatlem  39350  opelxpii  40213  hoicvr  44093  hoicvrrex  44101  ovnsubaddlem1  44115  ovnhoilem1  44146  ovnlecvr2  44155  opnvonmbllem1  44177  ovolval4lem2  44195  fnotaovb  44701  aovmpt4g  44704  rngccoALTV  45557  ringccoALTV  45620  rhmsubclem2  45656  rhmsubcALTVlem2  45674  rrx2plordisom  46080
  Copyright terms: Public domain W3C validator