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

Theorem opelxpi 5297
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 5295 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 218 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2131  cop 4319   × cxp 5256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-opab 4857  df-xp 5264
This theorem is referenced by:  opelxpd  5298  opelvvg  5314  opelvv  5315  opbrop  5347  elsnxp  5830  fnbrfvb2  6393  fpr2g  6631  fliftrel  6713  elovimad  6848  fnotovbOLD  6851  ov3  6954  ovres  6957  fovrn  6961  fnovrn  6966  ovima0  6970  ovconst2  6971  el2xptp0  7371  opiota  7388  oprab2co  7422  1stconst  7425  2ndconst  7426  seqomlem2  7707  brdifun  7932  ecopqsi  7963  brecop  7999  eceqoveq  8011  xpcomco  8207  xpf1o  8279  xpmapenlem  8284  unxpdomlem3  8323  djulcl  8936  djurcl  8937  djulf1o  8938  djurf1o  8939  djuun  8942  fseqenlem1  9029  fseqenlem2  9030  isfin4-3  9321  axdc4lem  9461  iundom2g  9546  canthp1lem2  9659  addpiord  9890  mulpiord  9891  pinq  9933  nqereu  9935  addpipq  9943  addpqnq  9944  mulpipq  9946  mulpqnq  9947  ordpipq  9948  addpqf  9950  mulpqf  9952  recmulnq  9970  dmrecnq  9974  ltexnq  9981  enreceq  10071  addsrpr  10080  mulsrpr  10081  0r  10085  1sr  10086  m1r  10087  addclsr  10088  mulclsr  10089  axaddf  10150  axmulf  10151  xrlenlt  10287  uzrdgfni  12943  swrdval  13608  cnrecnv  14096  ruclem1  15151  ruclem6  15155  eucalgf  15490  eucalg  15494  qnumdenbi  15646  crth  15677  phimullem  15678  prmreclem3  15816  setscom  16097  strfv2d  16099  setsid  16108  imasaddfnlem  16382  imasaddflem  16384  imasvscafn  16391  imasvscaval  16392  xpsaddlem  16429  xpsvsca  16433  xpsle  16435  comffval  16552  oppccofval  16569  isoval  16618  funcf2  16721  idfu2nd  16730  resf2nd  16748  wunfunc  16752  funcpropd  16753  fucco  16815  homaval  16874  setcco  16926  catcco  16944  estrcco  16963  xpcco  17016  xpchom2  17019  xpcco2  17020  xpccatid  17021  prfcl  17036  prf1st  17037  prf2nd  17038  catcxpccl  17040  evlf2  17051  curf1cl  17061  curf2cl  17064  curfcl  17065  uncf1  17069  uncf2  17070  uncfcurf  17072  diag11  17076  diag12  17077  diag2  17078  curf2ndf  17080  hof2fval  17088  yonedalem21  17106  yonedalem22  17111  yonedalem3b  17112  yonffthlem  17115  joindmss  17200  meetdmss  17214  latcl2  17241  latlem  17242  latjcom  17252  latmcom  17268  lsmhash  18310  efgmf  18318  efglem  18321  vrgpf  18373  vrgpinv  18374  frgpuplem  18377  frgpup2  18381  frgpnabllem1  18468  mamudi  20403  mamudir  20404  mamuvs1  20405  mamuvs2  20406  matsubgcell  20434  matvscacell  20436  mdetrsca  20603  pmatcoe1fsupp  20700  txbas  21564  txcls  21601  txcnp  21617  upxp  21620  txcnmpt  21621  uptx  21622  txlly  21633  txnlly  21634  txtube  21637  txcmplem1  21638  txlm  21645  lmcn2  21646  tx1stc  21647  txkgen  21649  xkococnlem  21656  cnmpt21  21668  txhmeo  21800  txswaphmeolem  21801  txswaphmeo  21802  ptuncnv  21804  txflf  22003  flfcnp2  22004  tmdcn2  22086  clssubg  22105  qustgplem  22117  tsmsadd  22143  imasdsf1olem  22371  xpsdsval  22379  comet  22511  txmetcnp  22545  metustid  22552  metustsym  22553  nrmmetd  22572  isngp3  22595  ngpds  22601  tngnm  22648  qtopbaslem  22755  cnmetdval  22767  remetdval  22785  tgqioo  22796  bndth  22950  htpyco2  22971  phtpyco2  22982  bcthlem5  23317  ovollb2lem  23448  ovolctb  23450  ovoliunlem2  23463  ovolscalem1  23473  ovolicc1  23476  ioombl1lem1  23518  ioorf  23533  ioorcl  23537  dyadf  23551  itg1addlem4  23657  limccnp2  23847  dvcnp2  23874  dvaddbr  23892  dvmulbr  23893  dvcobr  23900  dvef  23934  lhop1lem  23967  taylthlem2  24319  dvdsmulf1o  25111  tgelrnln  25716  brcgr  25971  imsdval  27842  sspval  27879  ofoprabco  29765  f1od2  29800  fimaproj  30201  qtophaus  30204  prsdm  30261  prsrn  30262  mbfmco2  30628  eulerpartlemgh  30741  afsval  31050  erdszelem9  31480  cvmlift2lem1  31583  cvmlift2lem9  31592  cvmlift2lem12  31595  cvmlift2lem13  31596  cvmliftphtlem  31598  msubco  31727  msubff1  31752  mvhf  31754  msubvrs  31756  fvtransport  32437  colinearex  32465  icoreunrn  33510  relowlpssretop  33515  cnfinltrel  33544  curf  33692  finixpnum  33699  poimirlem3  33717  poimirlem4  33718  poimirlem15  33729  poimirlem17  33731  poimirlem20  33734  poimirlem25  33739  poimirlem26  33740  poimirlem27  33741  heicant  33749  mblfinlem1  33751  mblfinlem2  33752  ftc1anc  33798  opropabco  33823  heiborlem5  33919  dvhelvbasei  36871  dvhopvadd  36876  dvhvaddcl  36878  dvhopvsca  36885  dvhvscacl  36886  dvhgrp  36890  dvhopclN  36896  dvhopaddN  36897  dvhopspN  36898  dib1dim2  36951  diblss  36953  diclspsn  36977  dih1dimatlem  37112  projf1o  39877  hoicvr  41260  hoicvrrex  41268  ovnsubaddlem1  41282  ovnhoilem1  41313  ovnlecvr2  41322  opnvonmbllem1  41344  ovolval4lem2  41362  fnotaovb  41776  aovmpt4g  41779  rngccoALTV  42490  ringccoALTV  42553  rhmsubclem2  42589  rhmsubcALTVlem2  42607
  Copyright terms: Public domain W3C validator