Theorem opelxpi 5675

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ⟨cop 4597   × cxp 5636

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5173  df-xp 5644

This theorem is referenced by:  opelxpd  5676  opelvv  5677  opelvvg  5678  opbrop  5734  elsnxp  6248  reuop  6250  fnbrfvb2  6904  ov3  7522  ovres  7525  fovcdm  7529  fnovrn  7534  ovima0  7538  ovconst2  7539  el2xptp0  7973  opiota  7996  fimaproj  8072  xpord2pred  8082  seqomlem2  8402  brdifun  8684  ecopqsi  8720  brecop  8756  eceqoveq  8768  xpcomco  9013  djulcl  9855  djurcl  9856  djulf1o  9857  djurf1o  9858  djuun  9871  isfin4p1  10260  axdc4lem  10400  canthp1lem2  10598  addpiord  10829  mulpiord  10830  pinq  10872  nqereu  10874  addpipq  10882  addpqnq  10883  mulpipq  10885  mulpqnq  10886  ordpipq  10887  recmulnq  10909  dmrecnq  10913  enreceq  11011  addsrpr  11020  mulsrpr  11021  0r  11025  1sr  11026  m1r  11027  addclsr  11028  mulclsr  11029  axaddf  11090  xrlenlt  11229  uzrdgfni  13873  swrdval  14543  ruclem6  16128  eucalgf  16470  eucalg  16474  qnumdenbi  16630  setscom  17063  strfv2d  17085  setsid  17091  imasaddfnlem  17424  imasaddflem  17426  imasvscafn  17433  imasvscaval  17434  funcpropd  17801  fucco  17865  catcxpccl  18109  catcxpcclOLD  18110  curf1cl  18131  curf2cl  18134  curfcl  18135  uncfcurf  18142  diag2  18148  curf2ndf  18150  joindmss  18282  meetdmss  18296  latlem  18340  latjcom  18350  latmcom  18366  efgmf  19509  efglem  19512  vrgpf  19564  vrgpinv  19565  frgpuplem  19568  frgpup2  19572  frgpnabllem1  19665  gsumxp2  19771  mamudi  21787  mamudir  21788  mamuvs1  21789  mamuvs2  21790  matsubgcell  21820  matvscacell  21822  pmatcoe1fsupp  22087  txbas  22955  txcls  22992  upxp  23011  uptx  23013  txtube  23028  txcmplem1  23029  txlm  23036  tx1stc  23038  txkgen  23040  cnmpt21  23059  txswaphmeolem  23192  txswaphmeo  23193  clssubg  23497  qustgplem  23509  comet  23906  txmetcnp  23940  metustsym  23948  nrmmetd  23967  isngp3  23991  ngpds  23997  qtopbaslem  24159  cnmetdval  24171  remetdval  24189  tgqioo  24200  bndth  24358  htpyco2  24379  phtpyco2  24390  ovolicc1  24917  ioorf  24974  ioorcl  24978  itg1addlem4  25100  itg1addlem4OLD  25101  dvcnp2  25321  dvef  25381  lhop1lem  25414  taylthlem2  25770  addsqnreup  26828  addsfo  27336  brcgr  27912  ex-fpar  29469  imsdval  29691  sspval  29728  opreu2reuALT  31469  2ndimaxp  31630  ofoprabco  31647  f1od2  31706  qtophaus  32506  mbfmco2  32954  eulerpartlemgh  33067  afsval  33373  erdszelem9  33880  cvmlift2lem1  33983  cvmlift2lem9  33992  cvmlift2lem12  33995  cvmlift2lem13  33996  cvmliftphtlem  33998  goel  34028  goelel3xp  34029  sat1el2xp  34060  fmla0xp  34064  prv1n  34112  msubco  34212  msubff1  34237  mvhf  34239  msubvrs  34241  fvtransport  34693  colinearex  34721  bj-idres  35704  icoreunrn  35903  relowlpssretop  35908  curf  36129  finixpnum  36136  poimirlem15  36166  poimirlem25  36176  poimirlem26  36177  poimirlem27  36178  heicant  36186  mblfinlem1  36188  mblfinlem2  36189  ftc1anc  36232  opropabco  36256  heiborlem5  36347  dvhelvbasei  39624  dvhopvadd  39629  dvhvaddcl  39631  dvhopvsca  39638  dvhvscacl  39639  dvhgrp  39643  dvhopclN  39649  dvhopaddN  39650  dvhopspN  39651  dib1dim2  39704  diblss  39706  diclspsn  39730  dih1dimatlem  39865  opelxpii  40726  hoicvr  44909  hoicvrrex  44917  ovnsubaddlem1  44931  ovnhoilem1  44962  ovnlecvr2  44971  opnvonmbllem1  44993  ovolval4lem2  45011  fnotaovb  45550  aovmpt4g  45553  rngccoALTV  46406  ringccoALTV  46469  rhmsubclem2  46505  rhmsubcALTVlem2  46523  rrx2plordisom  46929