Theorem opelxpi 5699

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ⟨cop 4600   × cxp 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5178  df-xp 5668

This theorem is referenced by:  opelxpii  5700  opelxpd  5701  opelvv  5702  opelvvg  5703  opbrop  5760  elsnxp  6293  reuop  6295  fnbrfvb2  6937  ov3  7574  ovres  7577  fovcdm  7581  fnovrn  7586  ovima0  7590  ovconst2  7591  el2xptp0  8033  opiota  8056  fimaproj  8131  xpord2pred  8141  seqomlem2  8438  brdifun  8725  ecopqsi  8768  brecop  8808  eceqoveq  8820  xpcomco  9055  djulcl  9896  djurcl  9897  djulf1o  9898  djurf1o  9899  djuun  9912  isfin4p1  10299  axdc4lem  10439  canthp1lem2  10638  addpiord  10869  mulpiord  10870  pinq  10912  nqereu  10914  addpipq  10922  addpqnq  10923  mulpipq  10925  mulpqnq  10926  ordpipq  10927  recmulnq  10949  dmrecnq  10953  enreceq  11051  addsrpr  11060  mulsrpr  11061  0r  11065  1sr  11066  m1r  11067  addclsr  11068  mulclsr  11069  axaddf  11130  xrlenlt  11274  uzrdgfni  13994  swrdval  14681  ruclem6  16291  eucalgf  16641  eucalg  16645  qnumdenbi  16803  setscom  17240  strfv2d  17261  setsid  17267  imasaddfnlem  17582  imasaddflem  17584  imasvscafn  17591  imasvscaval  17592  funcpropd  17959  fucco  18022  catcxpccl  18263  curf1cl  18284  curf2cl  18287  curfcl  18288  uncfcurf  18295  diag2  18301  curf2ndf  18303  joindmss  18433  meetdmss  18447  latlem  18493  latjcom  18503  latmcom  18519  efgmf  19783  efglem  19786  vrgpf  19838  vrgpinv  19839  frgpuplem  19842  frgpup2  19846  frgpnabllem1  19943  gsumxp2  20050  rhmsubclem2  20771  pzriprnglem10  21609  mamudi  22529  mamudir  22530  mamuvs1  22531  mamuvs2  22532  matsubgcell  22560  matvscacell  22562  pmatcoe1fsupp  22827  txbas  23693  txcls  23730  upxp  23749  uptx  23751  txtube  23766  txcmplem1  23767  txlm  23774  tx1stc  23776  txkgen  23778  cnmpt21  23797  txswaphmeolem  23930  txswaphmeo  23931  clssubg  24235  qustgplem  24247  comet  24639  txmetcnp  24673  metustsym  24681  nrmmetd  24700  isngp3  24724  ngpds  24730  qtopbaslem  24884  cnmetdval  24896  remetdval  24915  tgqioo  24926  bndth  25086  htpyco2  25107  phtpyco2  25118  ovolicc1  25644  ioorf  25701  ioorcl  25705  itg1addlem4  25827  dvcnp2  26048  dvef  26108  lhop1lem  26141  taylthlem2  26503  addsqnreup  27573  addsfo  28142  subsfo  28224  noseqrdgfn  28465  brcgr  29191  ex-fpar  30754  imsdval  30979  sspval  31016  opreu2reuALT  32764  2ndimaxp  32932  ofoprabco  32950  f1od2  33005  qtophaus  34171  mbfmco2  34600  eulerpartlemgh  34713  afsval  35006  erdszelem9  35624  cvmlift2lem1  35727  cvmlift2lem9  35736  cvmlift2lem12  35739  cvmlift2lem13  35740  cvmliftphtlem  35742  goel  35772  goelel3xp  35773  sat1el2xp  35804  fmla0xp  35808  prv1n  35856  msubco  35956  msubff1  35981  mvhf  35983  msubvrs  35985  fvtransport  36457  colinearex  36485  nmulprop  36615  bj-idres  37726  icoreunrn  37927  relowlpssretop  37932  curf  38171  finixpnum  38178  poimirlem15  38208  poimirlem25  38218  poimirlem26  38219  poimirlem27  38220  heicant  38228  mblfinlem1  38230  mblfinlem2  38231  ftc1anc  38274  opropabco  38297  heiborlem5  38388  dvhelvbasei  41786  dvhopvadd  41791  dvhvaddcl  41793  dvhopvsca  41800  dvhvscacl  41801  dvhgrp  41805  dvhopclN  41811  dvhopaddN  41812  dvhopspN  41813  dib1dim2  41866  diblss  41868  diclspsn  41892  dih1dimatlem  42027  hoicvrrex  47196  ovnsubaddlem1  47210  ovnhoilem1  47241  ovnlecvr2  47250  opnvonmbllem1  47272  ovolval4lem2  47290  fnotaovb  47858  aovmpt4g  47861  rngccoALTV  48959  rhmsubcALTVlem2  48970  ringccoALTV  48993  rrx2plordisom  49422