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

Theorem opelxpi 5146
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 5144 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 218 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1989  cop 4181   × cxp 5110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-opab 4711  df-xp 5118
This theorem is referenced by:  opelxpd  5147  opelvvg  5163  opelvv  5164  opbrop  5196  elsnxp  5675  fpr2g  6472  fliftrel  6555  elovimad  6690  fnotovb  6691  ov3  6794  ovres  6797  fovrn  6801  fnovrn  6806  ovima0  6810  ovconst2  6811  el2xptp0  7209  opiota  7226  oprab2co  7259  1stconst  7262  2ndconst  7263  seqomlem2  7543  brdifun  7768  ecopqsi  7801  brecop  7837  eceqoveq  7850  xpcomco  8047  xpf1o  8119  xpmapenlem  8124  unxpdomlem3  8163  fseqenlem1  8844  fseqenlem2  8845  isfin4-3  9134  axdc4lem  9274  iundom2g  9359  canthp1lem2  9472  addpiord  9703  mulpiord  9704  pinq  9746  nqereu  9748  addpipq  9756  addpqnq  9757  mulpipq  9759  mulpqnq  9760  ordpipq  9761  addpqf  9763  mulpqf  9765  recmulnq  9783  dmrecnq  9787  ltexnq  9794  enreceq  9884  addsrpr  9893  mulsrpr  9894  0r  9898  1sr  9899  m1r  9900  addclsr  9901  mulclsr  9902  axaddf  9963  axmulf  9964  xrlenlt  10100  uzrdgfni  12752  swrdval  13411  cnrecnv  13899  ruclem1  14954  ruclem6  14958  eucalgf  15290  eucalg  15294  qnumdenbi  15446  crth  15477  phimullem  15478  prmreclem3  15616  setscom  15897  strfv2d  15899  setsid  15908  imasaddfnlem  16182  imasaddflem  16184  imasvscafn  16191  imasvscaval  16192  xpsaddlem  16229  xpsvsca  16233  xpsle  16235  comffval  16353  oppccofval  16370  isoval  16419  funcf2  16522  idfu2nd  16531  resf2nd  16549  wunfunc  16553  funcpropd  16554  fucco  16616  homaval  16675  setcco  16727  catcco  16745  estrcco  16764  xpcco  16817  xpchom2  16820  xpcco2  16821  xpccatid  16822  prfcl  16837  prf1st  16838  prf2nd  16839  catcxpccl  16841  evlf2  16852  curf1cl  16862  curf2cl  16865  curfcl  16866  uncf1  16870  uncf2  16871  uncfcurf  16873  diag11  16877  diag12  16878  diag2  16879  curf2ndf  16881  hof2fval  16889  yonedalem21  16907  yonedalem22  16912  yonedalem3b  16913  yonffthlem  16916  joindmss  17001  meetdmss  17015  latcl2  17042  latlem  17043  latjcom  17053  latmcom  17069  lsmhash  18112  efgmf  18120  efglem  18123  vrgpf  18175  vrgpinv  18176  frgpuplem  18179  frgpup2  18183  frgpnabllem1  18270  mamudi  20203  mamudir  20204  mamuvs1  20205  mamuvs2  20206  matsubgcell  20234  matvscacell  20236  mdetrsca  20403  pmatcoe1fsupp  20500  txbas  21364  txcls  21401  txcnp  21417  upxp  21420  txcnmpt  21421  uptx  21422  txlly  21433  txnlly  21434  txtube  21437  txcmplem1  21438  txlm  21445  lmcn2  21446  tx1stc  21447  txkgen  21449  xkococnlem  21456  cnmpt21  21468  txhmeo  21600  txswaphmeolem  21601  txswaphmeo  21602  ptuncnv  21604  txflf  21804  flfcnp2  21805  tmdcn2  21887  clssubg  21906  qustgplem  21918  tsmsadd  21944  imasdsf1olem  22172  xpsdsval  22180  comet  22312  txmetcnp  22346  metustid  22353  metustsym  22354  nrmmetd  22373  isngp3  22396  ngpds  22402  tngnm  22449  qtopbaslem  22556  cnmetdval  22568  remetdval  22586  tgqioo  22597  bndth  22751  htpyco2  22772  phtpyco2  22783  bcthlem5  23119  ovollb2lem  23250  ovolctb  23252  ovoliunlem2  23265  ovolscalem1  23275  ovolicc1  23278  ioombl1lem1  23320  ioorf  23335  ioorcl  23339  dyadf  23353  itg1addlem4  23460  limccnp2  23650  dvcnp2  23677  dvaddbr  23695  dvmulbr  23696  dvcobr  23703  dvef  23737  lhop1lem  23770  taylthlem2  24122  dvdsmulf1o  24914  tgelrnln  25519  brcgr  25774  imsdval  27525  sspval  27562  ofoprabco  29449  f1od2  29484  fimaproj  29885  qtophaus  29888  prsdm  29945  prsrn  29946  mbfmco2  30312  eulerpartlemgh  30425  afsval  30734  erdszelem9  31166  cvmlift2lem1  31269  cvmlift2lem9  31278  cvmlift2lem10  31279  cvmlift2lem12  31281  cvmlift2lem13  31282  cvmliftphtlem  31284  msubco  31413  msubff1  31438  mvhf  31440  msubvrs  31442  fvtransport  32123  colinearex  32151  icoreunrn  33187  relowlpssretop  33192  curf  33367  finixpnum  33374  poimirlem3  33392  poimirlem4  33393  poimirlem15  33404  poimirlem17  33406  poimirlem20  33409  poimirlem25  33414  poimirlem26  33415  poimirlem27  33416  heicant  33424  mblfinlem1  33426  mblfinlem2  33427  ftc1anc  33473  opropabco  33498  heiborlem5  33594  dvhelvbasei  36203  dvhopvadd  36208  dvhvaddcl  36210  dvhopvsca  36217  dvhvscacl  36218  dvhgrp  36222  dvhopclN  36228  dvhopaddN  36229  dvhopspN  36230  dib1dim2  36283  diblss  36285  diclspsn  36309  dih1dimatlem  36444  projf1o  39208  hoicvr  40531  hoicvrrex  40539  ovnsubaddlem1  40553  ovnhoilem1  40584  ovnlecvr2  40593  opnvonmbllem1  40615  ovolval4lem2  40633  fnotaovb  41047  aovmpt4g  41050  rngccoALTV  41759  ringccoALTV  41822  rhmsubclem2  41858  rhmsubcALTVlem2  41876
  Copyright terms: Public domain W3C validator