Theorem opelxpi 5659

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ⟨cop 4584   × cxp 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-opab 5159  df-xp 5628

This theorem is referenced by:  opelxpii  5660  opelxpd  5661  opelvv  5662  opelvvg  5663  opbrop  5720  elsnxp  6247  reuop  6249  fnbrfvb2  6887  ov3  7519  ovres  7522  fovcdm  7526  fnovrn  7531  ovima0  7535  ovconst2  7536  el2xptp0  7978  opiota  8001  fimaproj  8075  xpord2pred  8085  seqomlem2  8380  brdifun  8663  ecopqsi  8706  brecop  8745  eceqoveq  8757  xpcomco  8993  djulcl  9820  djurcl  9821  djulf1o  9822  djurf1o  9823  djuun  9836  isfin4p1  10223  axdc4lem  10363  canthp1lem2  10562  addpiord  10793  mulpiord  10794  pinq  10836  nqereu  10838  addpipq  10846  addpqnq  10847  mulpipq  10849  mulpqnq  10850  ordpipq  10851  recmulnq  10873  dmrecnq  10877  enreceq  10975  addsrpr  10984  mulsrpr  10985  0r  10989  1sr  10990  m1r  10991  addclsr  10992  mulclsr  10993  axaddf  11054  xrlenlt  11195  uzrdgfni  13879  swrdval  14565  ruclem6  16158  eucalgf  16508  eucalg  16512  qnumdenbi  16669  setscom  17105  strfv2d  17126  setsid  17132  imasaddfnlem  17447  imasaddflem  17449  imasvscafn  17456  imasvscaval  17457  funcpropd  17824  fucco  17887  catcxpccl  18128  curf1cl  18149  curf2cl  18152  curfcl  18153  uncfcurf  18160  diag2  18166  curf2ndf  18168  joindmss  18298  meetdmss  18312  latlem  18358  latjcom  18368  latmcom  18384  efgmf  19640  efglem  19643  vrgpf  19695  vrgpinv  19696  frgpuplem  19699  frgpup2  19703  frgpnabllem1  19800  gsumxp2  19907  rhmsubclem2  20617  pzriprnglem10  21443  mamudi  22345  mamudir  22346  mamuvs1  22347  mamuvs2  22348  matsubgcell  22376  matvscacell  22378  pmatcoe1fsupp  22643  txbas  23509  txcls  23546  upxp  23565  uptx  23567  txtube  23582  txcmplem1  23583  txlm  23590  tx1stc  23592  txkgen  23594  cnmpt21  23613  txswaphmeolem  23746  txswaphmeo  23747  clssubg  24051  qustgplem  24063  comet  24455  txmetcnp  24489  metustsym  24497  nrmmetd  24516  isngp3  24540  ngpds  24546  qtopbaslem  24700  cnmetdval  24712  remetdval  24731  tgqioo  24742  bndth  24911  htpyco2  24932  phtpyco2  24943  ovolicc1  25471  ioorf  25528  ioorcl  25532  itg1addlem4  25654  dvcnp2  25875  dvcnp2OLD  25876  dvef  25938  lhop1lem  25972  taylthlem2  26336  taylthlem2OLD  26337  addsqnreup  27408  addsfo  27953  subsfo  28034  noseqrdgfn  28267  brcgr  28922  ex-fpar  30486  imsdval  30710  sspval  30747  opreu2reuALT  32500  2ndimaxp  32673  ofoprabco  32691  f1od2  32747  qtophaus  33942  mbfmco2  34371  eulerpartlemgh  34484  afsval  34777  erdszelem9  35342  cvmlift2lem1  35445  cvmlift2lem9  35454  cvmlift2lem12  35457  cvmlift2lem13  35458  cvmliftphtlem  35460  goel  35490  goelel3xp  35491  sat1el2xp  35522  fmla0xp  35526  prv1n  35574  msubco  35674  msubff1  35699  mvhf  35701  msubvrs  35703  fvtransport  36175  colinearex  36203  bj-idres  37304  icoreunrn  37503  relowlpssretop  37508  curf  37738  finixpnum  37745  poimirlem15  37775  poimirlem25  37785  poimirlem26  37786  poimirlem27  37787  heicant  37795  mblfinlem1  37797  mblfinlem2  37798  ftc1anc  37841  opropabco  37864  heiborlem5  37955  dvhelvbasei  41287  dvhopvadd  41292  dvhvaddcl  41294  dvhopvsca  41301  dvhvscacl  41302  dvhgrp  41306  dvhopclN  41312  dvhopaddN  41313  dvhopspN  41314  dib1dim2  41367  diblss  41369  diclspsn  41393  dih1dimatlem  41528  hoicvr  46734  hoicvrrex  46742  ovnsubaddlem1  46756  ovnhoilem1  46787  ovnlecvr2  46796  opnvonmbllem1  46818  ovolval4lem2  46836  fnotaovb  47386  aovmpt4g  47389  rngccoALTV  48459  rhmsubcALTVlem2  48470  ringccoALTV  48493  rrx2plordisom  48911