Theorem opelxpi 5556

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 5555	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 231	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ⟨cop 4531   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-xp 5525

This theorem is referenced by:  opelxpd  5557  opelvv  5558  opelvvg  5559  opbrop  5612  elsnxp  6110  reuop  6112  fnbrfvb2  6697  ov3  7291  ovres  7294  fovrn  7298  fnovrn  7303  ovima0  7307  ovconst2  7308  el2xptp0  7718  opiota  7739  fimaproj  7812  seqomlem2  8070  brdifun  8301  ecopqsi  8337  brecop  8373  eceqoveq  8385  xpcomco  8590  djulcl  9323  djurcl  9324  djulf1o  9325  djurf1o  9326  djuun  9339  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  13321  swrdval  13996  ruclem6  15580  eucalgf  15917  eucalg  15921  qnumdenbi  16074  setscom  16519  strfv2d  16521  setsid  16530  imasaddfnlem  16793  imasaddflem  16795  imasvscafn  16802  imasvscaval  16803  funcpropd  17162  fucco  17224  catcxpccl  17449  curf1cl  17470  curf2cl  17473  curfcl  17474  uncfcurf  17481  diag2  17487  curf2ndf  17489  joindmss  17609  meetdmss  17623  latlem  17651  latjcom  17661  latmcom  17677  efgmf  18831  efglem  18834  vrgpf  18886  vrgpinv  18887  frgpuplem  18890  frgpup2  18894  frgpnabllem1  18986  gsumxp2  19093  mamudi  21008  mamudir  21009  mamuvs1  21010  mamuvs2  21011  matsubgcell  21039  matvscacell  21041  pmatcoe1fsupp  21306  txbas  22172  txcls  22209  upxp  22228  uptx  22230  txtube  22245  txcmplem1  22246  txlm  22253  tx1stc  22255  txkgen  22257  cnmpt21  22276  txswaphmeolem  22409  txswaphmeo  22410  clssubg  22714  qustgplem  22726  comet  23120  txmetcnp  23154  metustsym  23162  nrmmetd  23181  isngp3  23204  ngpds  23210  qtopbaslem  23364  cnmetdval  23376  remetdval  23394  tgqioo  23405  bndth  23563  htpyco2  23584  phtpyco2  23595  ovolicc1  24120  ioorf  24177  ioorcl  24181  itg1addlem4  24303  dvcnp2  24523  dvef  24583  lhop1lem  24616  taylthlem2  24969  addsqnreup  26027  brcgr  26694  ex-fpar  28247  imsdval  28469  sspval  28506  opreu2reuALT  30247  2ndimaxp  30409  ofoprabco  30427  f1od2  30483  qtophaus  31189  mbfmco2  31633  eulerpartlemgh  31746  afsval  32052  erdszelem9  32559  cvmlift2lem1  32662  cvmlift2lem9  32671  cvmlift2lem12  32674  cvmlift2lem13  32675  cvmliftphtlem  32677  goel  32707  goelel3xp  32708  sat1el2xp  32739  fmla0xp  32743  prv1n  32791  msubco  32891  msubff1  32916  mvhf  32918  msubvrs  32920  fvtransport  33606  colinearex  33634  bj-idres  34575  icoreunrn  34776  relowlpssretop  34781  curf  35035  finixpnum  35042  poimirlem3  35060  poimirlem4  35061  poimirlem15  35072  poimirlem17  35074  poimirlem20  35077  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  heicant  35092  mblfinlem1  35094  mblfinlem2  35095  ftc1anc  35138  opropabco  35162  heiborlem5  35253  dvhelvbasei  38384  dvhopvadd  38389  dvhvaddcl  38391  dvhopvsca  38398  dvhvscacl  38399  dvhgrp  38403  dvhopclN  38409  dvhopaddN  38410  dvhopspN  38411  dib1dim2  38464  diblss  38466  diclspsn  38490  dih1dimatlem  38625  opelxpii  39411  hoicvr  43187  hoicvrrex  43195  ovnsubaddlem1  43209  ovnhoilem1  43240  ovnlecvr2  43249  opnvonmbllem1  43271  ovolval4lem2  43289  fnotaovb  43754  aovmpt4g  43757  rngccoALTV  44612  ringccoALTV  44675  rhmsubclem2  44711  rhmsubcALTVlem2  44729  rrx2plordisom  45137