Theorem opelxpi 5658

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ⟨cop 4564   × cxp 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5138  df-xp 5627

This theorem is referenced by:  opelxpii  5659  opelxpd  5660  opelvv  5661  opelvvg  5662  opbrop  5719  elsnxp  6246  reuop  6248  fnbrfvb2  6886  ov3  7523  ovres  7526  fovcdm  7530  fnovrn  7535  ovima0  7539  ovconst2  7540  el2xptp0  7982  opiota  8005  fimaproj  8079  xpord2pred  8089  seqomlem2  8384  brdifun  8668  ecopqsi  8711  brecop  8751  eceqoveq  8763  xpcomco  8999  djulcl  9829  djurcl  9830  djulf1o  9831  djurf1o  9832  djuun  9845  isfin4p1  10232  axdc4lem  10372  canthp1lem2  10571  addpiord  10802  mulpiord  10803  pinq  10845  nqereu  10847  addpipq  10855  addpqnq  10856  mulpipq  10858  mulpqnq  10859  ordpipq  10860  recmulnq  10882  dmrecnq  10886  enreceq  10984  addsrpr  10993  mulsrpr  10994  0r  10998  1sr  10999  m1r  11000  addclsr  11001  mulclsr  11002  axaddf  11063  xrlenlt  11205  uzrdgfni  13915  swrdval  14601  ruclem6  16197  eucalgf  16547  eucalg  16551  qnumdenbi  16709  setscom  17145  strfv2d  17166  setsid  17172  imasaddfnlem  17487  imasaddflem  17489  imasvscafn  17496  imasvscaval  17497  funcpropd  17864  fucco  17927  catcxpccl  18168  curf1cl  18189  curf2cl  18192  curfcl  18193  uncfcurf  18200  diag2  18206  curf2ndf  18208  joindmss  18338  meetdmss  18352  latlem  18398  latjcom  18408  latmcom  18424  efgmf  19683  efglem  19686  vrgpf  19738  vrgpinv  19739  frgpuplem  19742  frgpup2  19746  frgpnabllem1  19843  gsumxp2  19950  rhmsubclem2  20662  pzriprnglem10  21469  mamudi  22390  mamudir  22391  mamuvs1  22392  mamuvs2  22393  matsubgcell  22421  matvscacell  22423  pmatcoe1fsupp  22688  txbas  23554  txcls  23591  upxp  23610  uptx  23612  txtube  23627  txcmplem1  23628  txlm  23635  tx1stc  23637  txkgen  23639  cnmpt21  23658  txswaphmeolem  23791  txswaphmeo  23792  clssubg  24096  qustgplem  24108  comet  24500  txmetcnp  24534  metustsym  24542  nrmmetd  24561  isngp3  24585  ngpds  24591  qtopbaslem  24745  cnmetdval  24757  remetdval  24776  tgqioo  24787  bndth  24947  htpyco2  24968  phtpyco2  24979  ovolicc1  25505  ioorf  25562  ioorcl  25566  itg1addlem4  25688  dvcnp2  25909  dvef  25969  lhop1lem  26002  taylthlem2  26361  addsqnreup  27428  addsfo  27997  subsfo  28079  noseqrdgfn  28320  brcgr  28991  ex-fpar  30554  imsdval  30779  sspval  30816  opreu2reuALT  32568  2ndimaxp  32742  ofoprabco  32760  f1od2  32815  qtophaus  34032  mbfmco2  34461  eulerpartlemgh  34574  afsval  34870  erdszelem9  35442  cvmlift2lem1  35545  cvmlift2lem9  35554  cvmlift2lem12  35557  cvmlift2lem13  35558  cvmliftphtlem  35560  goel  35590  goelel3xp  35591  sat1el2xp  35622  fmla0xp  35626  prv1n  35674  msubco  35774  msubff1  35799  mvhf  35801  msubvrs  35803  fvtransport  36275  colinearex  36303  bj-idres  37535  icoreunrn  37736  relowlpssretop  37741  curf  37980  finixpnum  37987  poimirlem15  38017  poimirlem25  38027  poimirlem26  38028  poimirlem27  38029  heicant  38037  mblfinlem1  38039  mblfinlem2  38040  ftc1anc  38083  opropabco  38106  heiborlem5  38197  dvhelvbasei  41595  dvhopvadd  41600  dvhvaddcl  41602  dvhopvsca  41609  dvhvscacl  41610  dvhgrp  41614  dvhopclN  41620  dvhopaddN  41621  dvhopspN  41622  dib1dim2  41675  diblss  41677  diclspsn  41701  dih1dimatlem  41836  hoicvrrex  47013  ovnsubaddlem1  47027  ovnhoilem1  47058  ovnlecvr2  47067  opnvonmbllem1  47089  ovolval4lem2  47107  fnotaovb  47675  aovmpt4g  47678  rngccoALTV  48776  rhmsubcALTVlem2  48787  ringccoALTV  48810  rrx2plordisom  49228