Theorem opelxpi 5663

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

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

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 5232  ax-pr 5372

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-xp 5632

This theorem is referenced by:  opelxpii  5664  opelxpd  5665  opelvv  5666  opelvvg  5667  opbrop  5724  elsnxp  6251  reuop  6253  fnbrfvb2  6891  ov3  7525  ovres  7528  fovcdm  7532  fnovrn  7537  ovima0  7541  ovconst2  7542  el2xptp0  7984  opiota  8007  fimaproj  8080  xpord2pred  8090  seqomlem2  8385  brdifun  8669  ecopqsi  8712  brecop  8752  eceqoveq  8764  xpcomco  9000  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  20658  pzriprnglem10  21484  mamudi  22382  mamudir  22383  mamuvs1  22384  mamuvs2  22385  matsubgcell  22413  matvscacell  22415  pmatcoe1fsupp  22680  txbas  23546  txcls  23583  upxp  23602  uptx  23604  txtube  23619  txcmplem1  23620  txlm  23627  tx1stc  23629  txkgen  23631  cnmpt21  23650  txswaphmeolem  23783  txswaphmeo  23784  clssubg  24088  qustgplem  24100  comet  24492  txmetcnp  24526  metustsym  24534  nrmmetd  24553  isngp3  24577  ngpds  24583  qtopbaslem  24737  cnmetdval  24749  remetdval  24768  tgqioo  24779  bndth  24939  htpyco2  24960  phtpyco2  24971  ovolicc1  25497  ioorf  25554  ioorcl  25558  itg1addlem4  25680  dvcnp2  25901  dvef  25961  lhop1lem  25994  taylthlem2  26355  taylthlem2OLD  26356  addsqnreup  27424  addsfo  27993  subsfo  28075  noseqrdgfn  28316  brcgr  28987  ex-fpar  30551  imsdval  30776  sspval  30813  opreu2reuALT  32565  2ndimaxp  32738  ofoprabco  32756  f1od2  32811  qtophaus  34000  mbfmco2  34429  eulerpartlemgh  34542  afsval  34835  erdszelem9  35401  cvmlift2lem1  35504  cvmlift2lem9  35513  cvmlift2lem12  35516  cvmlift2lem13  35517  cvmliftphtlem  35519  goel  35549  goelel3xp  35550  sat1el2xp  35581  fmla0xp  35585  prv1n  35633  msubco  35733  msubff1  35758  mvhf  35760  msubvrs  35762  fvtransport  36234  colinearex  36262  bj-idres  37494  icoreunrn  37693  relowlpssretop  37698  curf  37937  finixpnum  37944  poimirlem15  37974  poimirlem25  37984  poimirlem26  37985  poimirlem27  37986  heicant  37994  mblfinlem1  37996  mblfinlem2  37997  ftc1anc  38040  opropabco  38063  heiborlem5  38154  dvhelvbasei  41552  dvhopvadd  41557  dvhvaddcl  41559  dvhopvsca  41566  dvhvscacl  41567  dvhgrp  41571  dvhopclN  41577  dvhopaddN  41578  dvhopspN  41579  dib1dim2  41632  diblss  41634  diclspsn  41658  dih1dimatlem  41793  hoicvrrex  47006  ovnsubaddlem1  47020  ovnhoilem1  47051  ovnlecvr2  47060  opnvonmbllem1  47082  ovolval4lem2  47100  fnotaovb  47662  aovmpt4g  47665  rngccoALTV  48763  rhmsubcALTVlem2  48774  ringccoALTV  48797  rrx2plordisom  49215