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

Theorem opelxpi 5605
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 5604 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 231 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  cop 4563   × cxp 5566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pr 5338
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-nul 4254  df-if 4456  df-sn 4558  df-pr 4560  df-op 4564  df-opab 5132  df-xp 5574
This theorem is referenced by:  opelxpd  5606  opelvv  5607  opelvvg  5608  opbrop  5662  elsnxp  6171  reuop  6173  fnbrfvb2  6790  ov3  7392  ovres  7395  fovrn  7399  fnovrn  7404  ovima0  7408  ovconst2  7409  el2xptp0  7829  opiota  7850  fimaproj  7925  seqomlem2  8210  brdifun  8443  ecopqsi  8479  brecop  8515  eceqoveq  8527  xpcomco  8760  djulcl  9555  djurcl  9556  djulf1o  9557  djurf1o  9558  djuun  9571  isfin4p1  9958  axdc4lem  10098  canthp1lem2  10296  addpiord  10527  mulpiord  10528  pinq  10570  nqereu  10572  addpipq  10580  addpqnq  10581  mulpipq  10583  mulpqnq  10584  ordpipq  10585  recmulnq  10607  dmrecnq  10611  enreceq  10709  addsrpr  10718  mulsrpr  10719  0r  10723  1sr  10724  m1r  10725  addclsr  10726  mulclsr  10727  axaddf  10788  xrlenlt  10927  uzrdgfni  13562  swrdval  14240  ruclem6  15828  eucalgf  16172  eucalg  16176  qnumdenbi  16332  setscom  16765  strfv2d  16784  setsid  16790  imasaddfnlem  17065  imasaddflem  17067  imasvscafn  17074  imasvscaval  17075  funcpropd  17439  fucco  17503  catcxpccl  17746  catcxpcclOLD  17747  curf1cl  17768  curf2cl  17771  curfcl  17772  uncfcurf  17779  diag2  17785  curf2ndf  17787  joindmss  17917  meetdmss  17931  latlem  17975  latjcom  17985  latmcom  18001  efgmf  19135  efglem  19138  vrgpf  19190  vrgpinv  19191  frgpuplem  19194  frgpup2  19198  frgpnabllem1  19290  gsumxp2  19397  mamudi  21331  mamudir  21332  mamuvs1  21333  mamuvs2  21334  matsubgcell  21362  matvscacell  21364  pmatcoe1fsupp  21629  txbas  22495  txcls  22532  upxp  22551  uptx  22553  txtube  22568  txcmplem1  22569  txlm  22576  tx1stc  22578  txkgen  22580  cnmpt21  22599  txswaphmeolem  22732  txswaphmeo  22733  clssubg  23037  qustgplem  23049  comet  23442  txmetcnp  23476  metustsym  23484  nrmmetd  23503  isngp3  23527  ngpds  23533  qtopbaslem  23687  cnmetdval  23699  remetdval  23717  tgqioo  23728  bndth  23886  htpyco2  23907  phtpyco2  23918  ovolicc1  24444  ioorf  24501  ioorcl  24505  itg1addlem4  24627  itg1addlem4OLD  24628  dvcnp2  24848  dvef  24908  lhop1lem  24941  taylthlem2  25297  addsqnreup  26355  brcgr  27022  ex-fpar  28576  imsdval  28798  sspval  28835  opreu2reuALT  30575  2ndimaxp  30734  ofoprabco  30752  f1od2  30807  qtophaus  31531  mbfmco2  31975  eulerpartlemgh  32088  afsval  32394  erdszelem9  32904  cvmlift2lem1  33007  cvmlift2lem9  33016  cvmlift2lem12  33019  cvmlift2lem13  33020  cvmliftphtlem  33022  goel  33052  goelel3xp  33053  sat1el2xp  33084  fmla0xp  33088  prv1n  33136  msubco  33236  msubff1  33261  mvhf  33263  msubvrs  33265  xpord2pred  33562  fvtransport  34104  colinearex  34132  bj-idres  35101  icoreunrn  35303  relowlpssretop  35308  curf  35528  finixpnum  35535  poimirlem15  35565  poimirlem25  35575  poimirlem26  35576  poimirlem27  35577  heicant  35585  mblfinlem1  35587  mblfinlem2  35588  ftc1anc  35631  opropabco  35655  heiborlem5  35746  dvhelvbasei  38875  dvhopvadd  38880  dvhvaddcl  38882  dvhopvsca  38889  dvhvscacl  38890  dvhgrp  38894  dvhopclN  38900  dvhopaddN  38901  dvhopspN  38902  dib1dim2  38955  diblss  38957  diclspsn  38981  dih1dimatlem  39116  opelxpii  39967  hoicvr  43806  hoicvrrex  43814  ovnsubaddlem1  43828  ovnhoilem1  43859  ovnlecvr2  43868  opnvonmbllem1  43890  ovolval4lem2  43908  fnotaovb  44407  aovmpt4g  44410  rngccoALTV  45264  ringccoALTV  45327  rhmsubclem2  45363  rhmsubcALTVlem2  45381  rrx2plordisom  45787
  Copyright terms: Public domain W3C validator