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

Theorem opelxpi 5586
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 5585 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 229 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  cop 4565   × cxp 5547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-opab 5121  df-xp 5555
This theorem is referenced by:  opelxpd  5587  opelvv  5588  opelvvg  5589  opbrop  5642  elsnxp  6136  reuop  6138  fnbrfvb2  6716  ov3  7300  ovres  7303  fovrn  7307  fnovrn  7312  ovima0  7316  ovconst2  7317  el2xptp0  7727  opiota  7748  fimaproj  7820  seqomlem2  8078  brdifun  8308  ecopqsi  8344  brecop  8380  eceqoveq  8392  xpcomco  8596  djulcl  9328  djurcl  9329  djulf1o  9330  djurf1o  9331  djuun  9344  isfin4p1  9726  axdc4lem  9866  canthp1lem2  10064  addpiord  10295  mulpiord  10296  pinq  10338  nqereu  10340  addpipq  10348  addpqnq  10349  mulpipq  10351  mulpqnq  10352  ordpipq  10353  recmulnq  10375  dmrecnq  10379  enreceq  10477  addsrpr  10486  mulsrpr  10487  0r  10491  1sr  10492  m1r  10493  addclsr  10494  mulclsr  10495  axaddf  10556  xrlenlt  10695  uzrdgfni  13316  swrdval  13995  ruclem6  15578  eucalgf  15917  eucalg  15921  qnumdenbi  16074  setscom  16517  strfv2d  16519  setsid  16528  imasaddfnlem  16791  imasaddflem  16793  imasvscafn  16800  imasvscaval  16801  funcpropd  17160  fucco  17222  catcxpccl  17447  curf1cl  17468  curf2cl  17471  curfcl  17472  uncfcurf  17479  diag2  17485  curf2ndf  17487  joindmss  17607  meetdmss  17621  latlem  17649  latjcom  17659  latmcom  17675  efgmf  18770  efglem  18773  vrgpf  18825  vrgpinv  18826  frgpuplem  18829  frgpup2  18833  frgpnabllem1  18924  gsumxp2  19031  mamudi  20942  mamudir  20943  mamuvs1  20944  mamuvs2  20945  matsubgcell  20973  matvscacell  20975  pmatcoe1fsupp  21239  txbas  22105  txcls  22142  upxp  22161  uptx  22163  txtube  22178  txcmplem1  22179  txlm  22186  tx1stc  22188  txkgen  22190  cnmpt21  22209  txswaphmeolem  22342  txswaphmeo  22343  clssubg  22646  qustgplem  22658  comet  23052  txmetcnp  23086  metustsym  23094  nrmmetd  23113  isngp3  23136  ngpds  23142  qtopbaslem  23296  cnmetdval  23308  remetdval  23326  tgqioo  23337  bndth  23491  htpyco2  23512  phtpyco2  23523  ovolicc1  24046  ioorf  24103  ioorcl  24107  itg1addlem4  24229  dvcnp2  24446  dvef  24506  lhop1lem  24539  taylthlem2  24891  addsqnreup  25947  brcgr  26614  ex-fpar  28169  imsdval  28391  sspval  28428  opreu2reuALT  30168  ofoprabco  30338  f1od2  30384  qtophaus  31000  mbfmco2  31423  eulerpartlemgh  31536  afsval  31842  erdszelem9  32344  cvmlift2lem1  32447  cvmlift2lem9  32456  cvmlift2lem12  32459  cvmlift2lem13  32460  cvmliftphtlem  32462  goel  32492  goelel3xp  32493  sat1el2xp  32524  fmla0xp  32528  prv1n  32576  msubco  32676  msubff1  32701  mvhf  32703  msubvrs  32705  fvtransport  33391  colinearex  33419  bj-idres  34345  icoreunrn  34523  relowlpssretop  34528  curf  34752  finixpnum  34759  poimirlem3  34777  poimirlem4  34778  poimirlem15  34789  poimirlem17  34791  poimirlem20  34794  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  heicant  34809  mblfinlem1  34811  mblfinlem2  34812  ftc1anc  34857  opropabco  34882  heiborlem5  34976  dvhelvbasei  38106  dvhopvadd  38111  dvhvaddcl  38113  dvhopvsca  38120  dvhvscacl  38121  dvhgrp  38125  dvhopclN  38131  dvhopaddN  38132  dvhopspN  38133  dib1dim2  38186  diblss  38188  diclspsn  38212  dih1dimatlem  38347  opelxpii  38997  hoicvr  42711  hoicvrrex  42719  ovnsubaddlem1  42733  ovnhoilem1  42764  ovnlecvr2  42773  opnvonmbllem1  42795  ovolval4lem2  42813  fnotaovb  43278  aovmpt4g  43281  rngccoALTV  44157  ringccoALTV  44220  rhmsubclem2  44256  rhmsubcALTVlem2  44274  rrx2plordisom  44608
  Copyright terms: Public domain W3C validator