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

Theorem opelxpi 5671
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 5670 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 227 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  cop 4593   × cxp 5632
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 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5169  df-xp 5640
This theorem is referenced by:  opelxpd  5672  opelvv  5673  opelvvg  5674  opbrop  5730  elsnxp  6244  reuop  6246  fnbrfvb2  6900  ov3  7518  ovres  7521  fovcdm  7525  fnovrn  7530  ovima0  7534  ovconst2  7535  el2xptp0  7969  opiota  7992  fimaproj  8068  xpord2pred  8078  seqomlem2  8398  brdifun  8678  ecopqsi  8714  brecop  8750  eceqoveq  8762  xpcomco  9007  djulcl  9847  djurcl  9848  djulf1o  9849  djurf1o  9850  djuun  9863  isfin4p1  10252  axdc4lem  10392  canthp1lem2  10590  addpiord  10821  mulpiord  10822  pinq  10864  nqereu  10866  addpipq  10874  addpqnq  10875  mulpipq  10877  mulpqnq  10878  ordpipq  10879  recmulnq  10901  dmrecnq  10905  enreceq  11003  addsrpr  11012  mulsrpr  11013  0r  11017  1sr  11018  m1r  11019  addclsr  11020  mulclsr  11021  axaddf  11082  xrlenlt  11221  uzrdgfni  13864  swrdval  14532  ruclem6  16118  eucalgf  16460  eucalg  16464  qnumdenbi  16620  setscom  17053  strfv2d  17075  setsid  17081  imasaddfnlem  17411  imasaddflem  17413  imasvscafn  17420  imasvscaval  17421  funcpropd  17788  fucco  17852  catcxpccl  18096  catcxpcclOLD  18097  curf1cl  18118  curf2cl  18121  curfcl  18122  uncfcurf  18129  diag2  18135  curf2ndf  18137  joindmss  18269  meetdmss  18283  latlem  18327  latjcom  18337  latmcom  18353  efgmf  19496  efglem  19499  vrgpf  19551  vrgpinv  19552  frgpuplem  19555  frgpup2  19559  frgpnabllem1  19652  gsumxp2  19758  mamudi  21753  mamudir  21754  mamuvs1  21755  mamuvs2  21756  matsubgcell  21786  matvscacell  21788  pmatcoe1fsupp  22053  txbas  22921  txcls  22958  upxp  22977  uptx  22979  txtube  22994  txcmplem1  22995  txlm  23002  tx1stc  23004  txkgen  23006  cnmpt21  23025  txswaphmeolem  23158  txswaphmeo  23159  clssubg  23463  qustgplem  23475  comet  23872  txmetcnp  23906  metustsym  23914  nrmmetd  23933  isngp3  23957  ngpds  23963  qtopbaslem  24125  cnmetdval  24137  remetdval  24155  tgqioo  24166  bndth  24324  htpyco2  24345  phtpyco2  24356  ovolicc1  24883  ioorf  24940  ioorcl  24944  itg1addlem4  25066  itg1addlem4OLD  25067  dvcnp2  25287  dvef  25347  lhop1lem  25380  taylthlem2  25736  addsqnreup  26794  addsfo  27296  brcgr  27852  ex-fpar  29409  imsdval  29631  sspval  29668  opreu2reuALT  31408  2ndimaxp  31566  ofoprabco  31583  f1od2  31641  qtophaus  32420  mbfmco2  32868  eulerpartlemgh  32981  afsval  33287  erdszelem9  33796  cvmlift2lem1  33899  cvmlift2lem9  33908  cvmlift2lem12  33911  cvmlift2lem13  33912  cvmliftphtlem  33914  goel  33944  goelel3xp  33945  sat1el2xp  33976  fmla0xp  33980  prv1n  34028  msubco  34128  msubff1  34153  mvhf  34155  msubvrs  34157  fvtransport  34620  colinearex  34648  bj-idres  35634  icoreunrn  35833  relowlpssretop  35838  curf  36059  finixpnum  36066  poimirlem15  36096  poimirlem25  36106  poimirlem26  36107  poimirlem27  36108  heicant  36116  mblfinlem1  36118  mblfinlem2  36119  ftc1anc  36162  opropabco  36186  heiborlem5  36277  dvhelvbasei  39554  dvhopvadd  39559  dvhvaddcl  39561  dvhopvsca  39568  dvhvscacl  39569  dvhgrp  39573  dvhopclN  39579  dvhopaddN  39580  dvhopspN  39581  dib1dim2  39634  diblss  39636  diclspsn  39660  dih1dimatlem  39795  opelxpii  40658  hoicvr  44796  hoicvrrex  44804  ovnsubaddlem1  44818  ovnhoilem1  44849  ovnlecvr2  44858  opnvonmbllem1  44880  ovolval4lem2  44898  fnotaovb  45437  aovmpt4g  45440  rngccoALTV  46293  ringccoALTV  46356  rhmsubclem2  46392  rhmsubcALTVlem2  46410  rrx2plordisom  46816
  Copyright terms: Public domain W3C validator