Theorem opelxpi 5072

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ⟨cop 4131   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-opab 4644  df-xp 5044

This theorem is referenced by:  opelxpd  5073  opelvvg  5087  opelvv  5088  opbrop  5121  elsnxp  5594  fpr2g  6380  fliftrel  6458  elovimad  6591  fnotovb  6592  ov3  6695  ovres  6698  fovrn  6702  fnovrn  6707  ovima0  6711  ovconst2  6712  opabex2  6997  el2xptp0  7103  opiota  7118  oprab2co  7149  1stconst  7152  2ndconst  7153  fnwelem  7179  seqomlem2  7433  brdifun  7658  ecopqsi  7691  brecop  7727  eceqoveq  7740  xpcomco  7935  xpf1o  8007  xpmapenlem  8012  unxpdomlem3  8051  fseqenlem1  8730  fseqenlem2  8731  isfin4-3  9020  axdc4lem  9160  iundom2g  9241  canthp1lem2  9354  addpiord  9585  mulpiord  9586  pinq  9628  nqereu  9630  addpipq  9638  addpqnq  9639  mulpipq  9641  mulpqnq  9642  ordpipq  9643  addpqf  9645  mulpqf  9647  recmulnq  9665  dmrecnq  9669  ltexnq  9676  enreceq  9766  addsrpr  9775  mulsrpr  9776  0r  9780  1sr  9781  m1r  9782  addclsr  9783  mulclsr  9784  axaddf  9845  axmulf  9846  xrlenlt  9982  uzrdgfni  12619  swrdval  13269  cnrecnv  13753  ruclem1  14799  ruclem6  14803  eucalgf  15134  eucalg  15138  qredeu  15210  qnumdenbi  15290  crth  15321  phimullem  15322  prmreclem3  15460  setscom  15731  strfv2d  15733  setsid  15742  imasaddfnlem  16011  imasaddflem  16013  imasvscafn  16020  imasvscaval  16021  xpsaddlem  16058  xpsvsca  16062  xpsle  16064  comffval  16182  oppccofval  16199  isoval  16248  funcf2  16351  idfu2nd  16360  resf2nd  16378  wunfunc  16382  funcpropd  16383  fucco  16445  homaval  16504  setcco  16556  catcco  16574  estrcco  16593  xpcco  16646  xpchom2  16649  xpcco2  16650  xpccatid  16651  prfcl  16666  prf1st  16667  prf2nd  16668  catcxpccl  16670  evlf2  16681  curf1cl  16691  curf2cl  16694  curfcl  16695  uncf1  16699  uncf2  16700  uncfcurf  16702  diag11  16706  diag12  16707  diag2  16708  curf2ndf  16710  hof2fval  16718  yonedalem21  16736  yonedalem22  16741  yonedalem3b  16742  yonffthlem  16745  joindmss  16830  meetdmss  16844  latcl2  16871  latlem  16872  latjcom  16882  latmcom  16898  lsmhash  17941  efgmf  17949  efglem  17952  vrgpf  18004  vrgpinv  18005  frgpuplem  18008  frgpup2  18012  frgpnabllem1  18099  mamudi  20028  mamudir  20029  mamuvs1  20030  mamuvs2  20031  matsubgcell  20059  matvscacell  20061  mdetrsca  20228  pmatcoe1fsupp  20325  txbas  21180  txcls  21217  txcnp  21233  upxp  21236  txcnmpt  21237  uptx  21238  txlly  21249  txnlly  21250  txtube  21253  txcmplem1  21254  txlm  21261  lmcn2  21262  tx1stc  21263  txkgen  21265  xkococnlem  21272  cnmpt21  21284  txhmeo  21416  txswaphmeolem  21417  txswaphmeo  21418  ptuncnv  21420  txflf  21620  flfcnp2  21621  tmdcn2  21703  clssubg  21722  qustgplem  21734  tsmsadd  21760  imasdsf1olem  21988  xpsdsval  21996  comet  22128  txmetcnp  22162  metustid  22169  metustsym  22170  nrmmetd  22189  isngp3  22212  ngpds  22218  tngnm  22265  qtopbaslem  22372  cnmetdval  22384  remetdval  22400  tgqioo  22411  bndth  22565  htpyco2  22586  phtpyco2  22597  bcthlem5  22933  ovollb2lem  23063  ovolctb  23065  ovoliunlem2  23078  ovolscalem1  23088  ovolicc1  23091  ioombl1lem1  23133  ioorf  23147  ioorcl  23151  dyadf  23165  itg1addlem4  23272  limccnp2  23462  dvcnp2  23489  dvaddbr  23507  dvmulbr  23508  dvcobr  23515  dvef  23547  lhop1lem  23580  taylthlem2  23932  dvdsmulf1o  24720  tgelrnln  25325  brcgr  25580  imsdval  26925  sspval  26962  ofoprabco  28847  f1od2  28887  fimaproj  29228  qtophaus  29231  prsdm  29288  prsrn  29289  mbfmco2  29654  eulerpartlemgh  29767  afsval  30002  erdszelem9  30435  cvmlift2lem1  30538  cvmlift2lem9  30547  cvmlift2lem10  30548  cvmlift2lem12  30550  cvmlift2lem13  30551  cvmliftphtlem  30553  msubco  30682  msubff1  30707  mvhf  30709  msubvrs  30711  fvtransport  31309  colinearex  31337  icoreunrn  32383  relowlpssretop  32388  curf  32557  finixpnum  32564  poimirlem3  32582  poimirlem4  32583  poimirlem15  32594  poimirlem17  32596  poimirlem20  32599  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  heicant  32614  mblfinlem1  32616  mblfinlem2  32617  ftc1anc  32663  opropabco  32688  heiborlem5  32784  dvhelvbasei  35395  dvhopvadd  35400  dvhvaddcl  35402  dvhopvsca  35409  dvhvscacl  35410  dvhgrp  35414  dvhopclN  35420  dvhopaddN  35421  dvhopspN  35422  dib1dim2  35475  diblss  35477  diclspsn  35501  dih1dimatlem  35636  projf1o  38381  hoicvr  39438  hoicvrrex  39446  ovnsubaddlem1  39460  ovnhoilem1  39491  ovnlecvr2  39500  opnvonmbllem1  39522  ovolval4lem2  39540  fnotaovb  39927  aovmpt4g  39930  rngccoALTV  41780  ringccoALTV  41843  rhmsubclem2  41879  rhmsubcALTVlem2  41898