Theorem opelxpi 5726

Description: Ordered pair membership in a Cartesian product (implication). (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opelxpi	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpi

Step	Hyp	Ref	Expression
1		opelxp 5725	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 228	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106  ⟨cop 4637   × cxp 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-opab 5211  df-xp 5695

This theorem is referenced by:  opelxpii  5727  opelxpd  5728  opelvv  5729  opelvvg  5730  opbrop  5786  elsnxp  6313  reuop  6315  fnbrfvb2  6964  ov3  7596  ovres  7599  fovcdm  7603  fnovrn  7608  ovima0  7612  ovconst2  7613  el2xptp0  8060  opiota  8083  fimaproj  8159  xpord2pred  8169  seqomlem2  8490  brdifun  8774  ecopqsi  8813  brecop  8849  eceqoveq  8861  xpcomco  9101  djulcl  9948  djurcl  9949  djulf1o  9950  djurf1o  9951  djuun  9964  isfin4p1  10353  axdc4lem  10493  canthp1lem2  10691  addpiord  10922  mulpiord  10923  pinq  10965  nqereu  10967  addpipq  10975  addpqnq  10976  mulpipq  10978  mulpqnq  10979  ordpipq  10980  recmulnq  11002  dmrecnq  11006  enreceq  11104  addsrpr  11113  mulsrpr  11114  0r  11118  1sr  11119  m1r  11120  addclsr  11121  mulclsr  11122  axaddf  11183  xrlenlt  11324  uzrdgfni  13996  swrdval  14678  ruclem6  16268  eucalgf  16617  eucalg  16621  qnumdenbi  16778  setscom  17214  strfv2d  17236  setsid  17242  imasaddfnlem  17575  imasaddflem  17577  imasvscafn  17584  imasvscaval  17585  funcpropd  17954  fucco  18019  catcxpccl  18263  catcxpcclOLD  18264  curf1cl  18285  curf2cl  18288  curfcl  18289  uncfcurf  18296  diag2  18302  curf2ndf  18304  joindmss  18437  meetdmss  18451  latlem  18495  latjcom  18505  latmcom  18521  efgmf  19746  efglem  19749  vrgpf  19801  vrgpinv  19802  frgpuplem  19805  frgpup2  19809  frgpnabllem1  19906  gsumxp2  20013  rhmsubclem2  20703  pzriprnglem10  21519  mamudi  22423  mamudir  22424  mamuvs1  22425  mamuvs2  22426  matsubgcell  22456  matvscacell  22458  pmatcoe1fsupp  22723  txbas  23591  txcls  23628  upxp  23647  uptx  23649  txtube  23664  txcmplem1  23665  txlm  23672  tx1stc  23674  txkgen  23676  cnmpt21  23695  txswaphmeolem  23828  txswaphmeo  23829  clssubg  24133  qustgplem  24145  comet  24542  txmetcnp  24576  metustsym  24584  nrmmetd  24603  isngp3  24627  ngpds  24633  qtopbaslem  24795  cnmetdval  24807  remetdval  24825  tgqioo  24836  bndth  25004  htpyco2  25025  phtpyco2  25036  ovolicc1  25565  ioorf  25622  ioorcl  25626  itg1addlem4  25748  itg1addlem4OLD  25749  dvcnp2  25970  dvcnp2OLD  25971  dvef  26033  lhop1lem  26067  taylthlem2  26431  taylthlem2OLD  26432  addsqnreup  27502  addsfo  28031  subsfo  28110  noseqrdgfn  28327  brcgr  28930  ex-fpar  30491  imsdval  30715  sspval  30752  opreu2reuALT  32505  2ndimaxp  32663  ofoprabco  32681  f1od2  32739  qtophaus  33797  mbfmco2  34247  eulerpartlemgh  34360  afsval  34665  erdszelem9  35184  cvmlift2lem1  35287  cvmlift2lem9  35296  cvmlift2lem12  35299  cvmlift2lem13  35300  cvmliftphtlem  35302  goel  35332  goelel3xp  35333  sat1el2xp  35364  fmla0xp  35368  prv1n  35416  msubco  35516  msubff1  35541  mvhf  35543  msubvrs  35545  fvtransport  36014  colinearex  36042  bj-idres  37143  icoreunrn  37342  relowlpssretop  37347  curf  37585  finixpnum  37592  poimirlem15  37622  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  heicant  37642  mblfinlem1  37644  mblfinlem2  37645  ftc1anc  37688  opropabco  37711  heiborlem5  37802  dvhelvbasei  41071  dvhopvadd  41076  dvhvaddcl  41078  dvhopvsca  41085  dvhvscacl  41086  dvhgrp  41090  dvhopclN  41096  dvhopaddN  41097  dvhopspN  41098  dib1dim2  41151  diblss  41153  diclspsn  41177  dih1dimatlem  41312  hoicvr  46504  hoicvrrex  46512  ovnsubaddlem1  46526  ovnhoilem1  46557  ovnlecvr2  46566  opnvonmbllem1  46588  ovolval4lem2  46606  fnotaovb  47148  aovmpt4g  47151  rngccoALTV  48115  rhmsubcALTVlem2  48126  ringccoALTV  48149  rrx2plordisom  48573