Theorem opelxpi 5671

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ⟨cop 4588   × cxp 5632

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-xp 5640

This theorem is referenced by:  opelxpii  5672  opelxpd  5673  opelvv  5674  opelvvg  5675  opbrop  5732  elsnxp  6259  reuop  6261  fnbrfvb2  6899  ov3  7533  ovres  7536  fovcdm  7540  fnovrn  7545  ovima0  7549  ovconst2  7550  el2xptp0  7992  opiota  8015  fimaproj  8089  xpord2pred  8099  seqomlem2  8394  brdifun  8678  ecopqsi  8721  brecop  8761  eceqoveq  8773  xpcomco  9009  djulcl  9836  djurcl  9837  djulf1o  9838  djurf1o  9839  djuun  9852  isfin4p1  10239  axdc4lem  10379  canthp1lem2  10578  addpiord  10809  mulpiord  10810  pinq  10852  nqereu  10854  addpipq  10862  addpqnq  10863  mulpipq  10865  mulpqnq  10866  ordpipq  10867  recmulnq  10889  dmrecnq  10893  enreceq  10991  addsrpr  11000  mulsrpr  11001  0r  11005  1sr  11006  m1r  11007  addclsr  11008  mulclsr  11009  axaddf  11070  xrlenlt  11211  uzrdgfni  13895  swrdval  14581  ruclem6  16174  eucalgf  16524  eucalg  16528  qnumdenbi  16685  setscom  17121  strfv2d  17142  setsid  17148  imasaddfnlem  17463  imasaddflem  17465  imasvscafn  17472  imasvscaval  17473  funcpropd  17840  fucco  17903  catcxpccl  18144  curf1cl  18165  curf2cl  18168  curfcl  18169  uncfcurf  18176  diag2  18182  curf2ndf  18184  joindmss  18314  meetdmss  18328  latlem  18374  latjcom  18384  latmcom  18400  efgmf  19659  efglem  19662  vrgpf  19714  vrgpinv  19715  frgpuplem  19718  frgpup2  19722  frgpnabllem1  19819  gsumxp2  19926  rhmsubclem2  20636  pzriprnglem10  21462  mamudi  22364  mamudir  22365  mamuvs1  22366  mamuvs2  22367  matsubgcell  22395  matvscacell  22397  pmatcoe1fsupp  22662  txbas  23528  txcls  23565  upxp  23584  uptx  23586  txtube  23601  txcmplem1  23602  txlm  23609  tx1stc  23611  txkgen  23613  cnmpt21  23632  txswaphmeolem  23765  txswaphmeo  23766  clssubg  24070  qustgplem  24082  comet  24474  txmetcnp  24508  metustsym  24516  nrmmetd  24535  isngp3  24559  ngpds  24565  qtopbaslem  24719  cnmetdval  24731  remetdval  24750  tgqioo  24761  bndth  24930  htpyco2  24951  phtpyco2  24962  ovolicc1  25490  ioorf  25547  ioorcl  25551  itg1addlem4  25673  dvcnp2  25894  dvcnp2OLD  25895  dvef  25957  lhop1lem  25991  taylthlem2  26355  taylthlem2OLD  26356  addsqnreup  27427  addsfo  27996  subsfo  28078  noseqrdgfn  28319  brcgr  28991  ex-fpar  30555  imsdval  30780  sspval  30817  opreu2reuALT  32569  2ndimaxp  32742  ofoprabco  32760  f1od2  32815  qtophaus  34020  mbfmco2  34449  eulerpartlemgh  34562  afsval  34855  erdszelem9  35421  cvmlift2lem1  35524  cvmlift2lem9  35533  cvmlift2lem12  35536  cvmlift2lem13  35537  cvmliftphtlem  35539  goel  35569  goelel3xp  35570  sat1el2xp  35601  fmla0xp  35605  prv1n  35653  msubco  35753  msubff1  35778  mvhf  35780  msubvrs  35782  fvtransport  36254  colinearex  36282  bj-idres  37442  icoreunrn  37641  relowlpssretop  37646  curf  37878  finixpnum  37885  poimirlem15  37915  poimirlem25  37925  poimirlem26  37926  poimirlem27  37927  heicant  37935  mblfinlem1  37937  mblfinlem2  37938  ftc1anc  37981  opropabco  38004  heiborlem5  38095  dvhelvbasei  41493  dvhopvadd  41498  dvhvaddcl  41500  dvhopvsca  41507  dvhvscacl  41508  dvhgrp  41512  dvhopclN  41518  dvhopaddN  41519  dvhopspN  41520  dib1dim2  41573  diblss  41575  diclspsn  41599  dih1dimatlem  41734  hoicvrrex  46943  ovnsubaddlem1  46957  ovnhoilem1  46988  ovnlecvr2  46997  opnvonmbllem1  47019  ovolval4lem2  47037  fnotaovb  47587  aovmpt4g  47590  rngccoALTV  48660  rhmsubcALTVlem2  48671  ringccoALTV  48694  rrx2plordisom  49112