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

Theorem opelxpi 5355
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 5353 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 219 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2157  cop 4383   × cxp 5316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pr 5103
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-opab 4914  df-xp 5324
This theorem is referenced by:  opelxpd  5356  opelvvg  5372  opelvv  5373  opbrop  5407  elsnxp  5898  fnbrfvb2  6463  fpr2g  6703  fliftrel  6785  elovimad  6924  fnotovbOLD  6927  ov3  7030  ovres  7033  fovrn  7037  fnovrn  7042  ovima0  7046  ovconst2  7047  el2xptp0  7447  opiota  7464  oprab2co  7499  1stconst  7502  2ndconst  7503  seqomlem2  7785  brdifun  8011  ecopqsi  8042  brecop  8078  eceqoveq  8091  xpcomco  8292  xpf1o  8364  unxpdomlem3  8408  djulcl  9022  djurcl  9023  djulf1o  9024  djurf1o  9025  djuun  9038  fseqenlem1  9133  fseqenlem2  9134  isfin4-3  9425  axdc4lem  9565  iundom2g  9650  canthp1lem2  9763  addpiord  9994  mulpiord  9995  pinq  10037  nqereu  10039  addpipq  10047  addpqnq  10048  mulpipq  10050  mulpqnq  10051  ordpipq  10052  addpqf  10054  mulpqf  10056  recmulnq  10074  dmrecnq  10078  ltexnq  10085  enreceq  10175  addsrpr  10184  mulsrpr  10185  0r  10189  1sr  10190  m1r  10191  addclsr  10192  mulclsr  10193  axaddf  10254  axmulf  10255  xrlenlt  10391  uzrdgfni  12984  swrdval  13643  cnrecnv  14131  ruclem1  15183  ruclem6  15187  eucalgf  15518  eucalg  15522  qnumdenbi  15672  crth  15703  phimullem  15704  prmreclem3  15842  setscom  16117  strfv2d  16119  setsid  16128  imasaddfnlem  16396  imasaddflem  16398  imasvscafn  16405  imasvscaval  16406  xpsaddlem  16443  xpsvsca  16447  xpsle  16449  comffval  16566  oppccofval  16583  isoval  16632  funcf2  16735  idfu2nd  16744  resf2nd  16762  wunfunc  16766  funcpropd  16767  fucco  16829  homaval  16888  setcco  16940  catcco  16958  estrcco  16977  xpcco  17031  xpchom2  17034  xpcco2  17035  xpccatid  17036  prfcl  17051  prf1st  17052  prf2nd  17053  catcxpccl  17055  evlf2  17066  curf1cl  17076  curf2cl  17079  curfcl  17080  uncf1  17084  uncf2  17085  uncfcurf  17087  diag11  17091  diag12  17092  diag2  17093  curf2ndf  17095  hof2fval  17103  yonedalem21  17121  yonedalem22  17126  yonedalem3b  17127  yonffthlem  17130  joindmss  17215  meetdmss  17229  latcl2  17256  latlem  17257  latjcom  17267  latmcom  17283  lsmhash  18322  efgmf  18330  efglem  18333  vrgpf  18385  vrgpinv  18386  frgpuplem  18389  frgpup2  18393  frgpnabllem1  18480  mamudi  20423  mamudir  20424  mamuvs1  20425  mamuvs2  20426  matsubgcell  20454  matvscacell  20456  mdetrsca  20624  pmatcoe1fsupp  20723  txbas  21588  txcls  21625  txcnp  21641  upxp  21644  txcnmpt  21645  uptx  21646  txlly  21657  txnlly  21658  txtube  21661  txcmplem1  21662  txlm  21669  lmcn2  21670  tx1stc  21671  txkgen  21673  xkococnlem  21680  cnmpt21  21692  txhmeo  21824  txswaphmeolem  21825  txswaphmeo  21826  ptuncnv  21828  txflf  22027  flfcnp2  22028  tmdcn2  22110  clssubg  22129  qustgplem  22141  tsmsadd  22167  imasdsf1olem  22395  xpsdsval  22403  comet  22535  txmetcnp  22569  metustid  22576  metustsym  22577  nrmmetd  22596  isngp3  22619  ngpds  22625  tngnm  22672  qtopbaslem  22779  cnmetdval  22791  remetdval  22809  tgqioo  22820  bndth  22974  htpyco2  22995  phtpyco2  23006  bcthlem5  23342  ovollb2lem  23475  ovolctb  23477  ovoliunlem2  23490  ovolscalem1  23500  ovolicc1  23503  ioombl1lem1  23545  ioorf  23560  ioorcl  23564  dyadf  23578  itg1addlem4  23686  limccnp2  23876  dvcnp2  23903  dvaddbr  23921  dvmulbr  23922  dvcobr  23929  dvef  23963  lhop1lem  23996  taylthlem2  24348  dvdsmulf1o  25140  tgelrnln  25745  brcgr  26000  imsdval  27875  sspval  27912  ofoprabco  29797  f1od2  29832  fimaproj  30231  qtophaus  30234  prsdm  30291  prsrn  30292  mbfmco2  30658  eulerpartlemgh  30771  afsval  31080  erdszelem9  31509  cvmlift2lem1  31612  cvmlift2lem9  31621  cvmlift2lem12  31624  cvmlift2lem13  31625  cvmliftphtlem  31627  msubco  31756  msubff1  31781  mvhf  31783  msubvrs  31785  fvtransport  32465  colinearex  32493  icoreunrn  33525  relowlpssretop  33530  cnfinltrel  33559  curf  33702  finixpnum  33709  poimirlem3  33727  poimirlem4  33728  poimirlem15  33739  poimirlem17  33741  poimirlem20  33744  poimirlem25  33749  poimirlem26  33750  poimirlem27  33751  heicant  33759  mblfinlem1  33761  mblfinlem2  33762  ftc1anc  33807  opropabco  33832  heiborlem5  33927  dvhelvbasei  36870  dvhopvadd  36875  dvhvaddcl  36877  dvhopvsca  36884  dvhvscacl  36885  dvhgrp  36889  dvhopclN  36895  dvhopaddN  36896  dvhopspN  36897  dib1dim2  36950  diblss  36952  diclspsn  36976  dih1dimatlem  37111  opelxpii  37756  projf1o  39876  hoicvr  41245  hoicvrrex  41253  ovnsubaddlem1  41267  ovnhoilem1  41298  ovnlecvr2  41307  opnvonmbllem1  41329  ovolval4lem2  41347  fnotaovb  41788  aovmpt4g  41791  rngccoALTV  42557  ringccoALTV  42620  rhmsubclem2  42656  rhmsubcALTVlem2  42674
  Copyright terms: Public domain W3C validator