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

Theorem opelxpi 5059
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 5057 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 216 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  cop 4127   × cxp 5023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-opab 4635  df-xp 5031
This theorem is referenced by:  opelxpd  5060  opelvvg  5074  opelvv  5075  opbrop  5108  elsnxp  5577  fpr2g  6355  fliftrel  6433  elovimad  6566  fnotovb  6567  ov3  6670  ovres  6673  fovrn  6676  fnovrn  6681  ovima0  6685  ovconst2  6686  opabex2  6971  el2xptp0  7077  opiota  7092  oprab2co  7123  1stconst  7126  2ndconst  7127  fnwelem  7153  seqomlem2  7407  brdifun  7632  ecopqsi  7665  brecop  7701  eceqoveq  7714  xpcomco  7909  xpf1o  7981  xpmapenlem  7986  unxpdomlem3  8025  fseqenlem1  8704  fseqenlem2  8705  isfin4-3  8994  axdc4lem  9134  iundom2g  9215  canthp1lem2  9328  addpiord  9559  mulpiord  9560  pinq  9602  nqereu  9604  addpipq  9612  addpqnq  9613  mulpipq  9615  mulpqnq  9616  ordpipq  9617  addpqf  9619  mulpqf  9621  recmulnq  9639  dmrecnq  9643  ltexnq  9650  enreceq  9740  addsrpr  9749  mulsrpr  9750  0r  9754  1sr  9755  m1r  9756  addclsr  9757  mulclsr  9758  axaddf  9819  axmulf  9820  xrlenlt  9951  uzrdgfni  12571  swrdval  13212  cnrecnv  13696  ruclem1  14742  ruclem6  14746  eucalgf  15077  eucalg  15081  qredeu  15153  qnumdenbi  15233  crth  15264  phimullem  15265  prmreclem3  15403  setscom  15674  strfv2d  15676  setsid  15685  imasaddfnlem  15954  imasaddflem  15956  imasvscafn  15963  imasvscaval  15964  xpsaddlem  16001  xpsvsca  16005  xpsle  16007  comffval  16125  oppccofval  16142  isoval  16191  funcf2  16294  idfu2nd  16303  resf2nd  16321  wunfunc  16325  funcpropd  16326  fucco  16388  homaval  16447  setcco  16499  catcco  16517  estrcco  16536  xpcco  16589  xpchom2  16592  xpcco2  16593  xpccatid  16594  prfcl  16609  prf1st  16610  prf2nd  16611  catcxpccl  16613  evlf2  16624  curf1cl  16634  curf2cl  16637  curfcl  16638  uncf1  16642  uncf2  16643  uncfcurf  16645  diag11  16649  diag12  16650  diag2  16651  curf2ndf  16653  hof2fval  16661  yonedalem21  16679  yonedalem22  16684  yonedalem3b  16685  yonffthlem  16688  joindmss  16773  meetdmss  16787  latcl2  16814  latlem  16815  latjcom  16825  latmcom  16841  lsmhash  17884  efgmf  17892  efglem  17895  vrgpf  17947  vrgpinv  17948  frgpuplem  17951  frgpup2  17955  frgpnabllem1  18042  mamudi  19967  mamudir  19968  mamuvs1  19969  mamuvs2  19970  matsubgcell  19998  matvscacell  20000  mdetrsca  20167  pmatcoe1fsupp  20264  txbas  21119  txcls  21156  txcnp  21172  upxp  21175  txcnmpt  21176  uptx  21177  txlly  21188  txnlly  21189  txtube  21192  txcmplem1  21193  txlm  21200  lmcn2  21201  tx1stc  21202  txkgen  21204  xkococnlem  21211  cnmpt21  21223  txhmeo  21355  txswaphmeolem  21356  txswaphmeo  21357  ptuncnv  21359  txflf  21559  flfcnp2  21560  tmdcn2  21642  clssubg  21661  qustgplem  21673  tsmsadd  21699  imasdsf1olem  21926  xpsdsval  21934  comet  22066  txmetcnp  22100  metustid  22107  metustsym  22108  nrmmetd  22127  isngp3  22150  ngpds  22155  tngnm  22200  qtopbaslem  22301  cnmetdval  22313  remetdval  22329  tgqioo  22340  bndth  22493  htpyco2  22514  phtpyco2  22525  bcthlem5  22847  ovollb2lem  22977  ovolctb  22979  ovoliunlem2  22992  ovolscalem1  23002  ovolicc1  23005  ioombl1lem1  23047  ioorf  23061  ioorcl  23065  dyadf  23079  itg1addlem4  23186  limccnp2  23376  dvcnp2  23403  dvaddbr  23421  dvmulbr  23422  dvcobr  23429  dvef  23461  lhop1lem  23494  taylthlem2  23846  dvdsmulf1o  24634  tgelrnln  25240  brcgr  25495  imsdval  26719  sspval  26763  ofoprabco  28650  f1od2  28690  fimaproj  29031  qtophaus  29034  prsdm  29091  prsrn  29092  mbfmco2  29457  eulerpartlemgh  29570  afsval  29805  erdszelem9  30238  cvmlift2lem1  30341  cvmlift2lem9  30350  cvmlift2lem10  30351  cvmlift2lem12  30353  cvmlift2lem13  30354  cvmliftphtlem  30356  msubco  30485  msubff1  30510  mvhf  30512  msubvrs  30514  fvtransport  31112  colinearex  31140  icoreunrn  32183  relowlpssretop  32188  curf  32357  finixpnum  32364  poimirlem3  32382  poimirlem4  32383  poimirlem15  32394  poimirlem17  32396  poimirlem20  32399  poimirlem25  32404  poimirlem26  32405  poimirlem27  32406  heicant  32414  mblfinlem1  32416  mblfinlem2  32417  ftc1anc  32463  opropabco  32488  heiborlem5  32584  dvhelvbasei  35195  dvhopvadd  35200  dvhvaddcl  35202  dvhopvsca  35209  dvhvscacl  35210  dvhgrp  35214  dvhopclN  35220  dvhopaddN  35221  dvhopspN  35222  dib1dim2  35275  diblss  35277  diclspsn  35301  dih1dimatlem  35436  projf1o  38181  hoicvr  39239  hoicvrrex  39247  ovnsubaddlem1  39261  ovnhoilem1  39292  ovnlecvr2  39301  opnvonmbllem1  39323  ovolval4lem2  39341  fnotaovb  39729  aovmpt4g  39732  rngccoALTV  41779  ringccoALTV  41842  rhmsubclem2  41878  rhmsubcALTVlem2  41897
  Copyright terms: Public domain W3C validator