Theorem opelxpi 5651

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ⟨cop 4579   × cxp 5612

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-opab 5152  df-xp 5620

This theorem is referenced by:  opelxpii  5652  opelxpd  5653  opelvv  5654  opelvvg  5655  opbrop  5712  elsnxp  6238  reuop  6240  fnbrfvb2  6877  ov3  7509  ovres  7512  fovcdm  7516  fnovrn  7521  ovima0  7525  ovconst2  7526  el2xptp0  7968  opiota  7991  fimaproj  8065  xpord2pred  8075  seqomlem2  8370  brdifun  8652  ecopqsi  8695  brecop  8734  eceqoveq  8746  xpcomco  8980  djulcl  9803  djurcl  9804  djulf1o  9805  djurf1o  9806  djuun  9819  isfin4p1  10206  axdc4lem  10346  canthp1lem2  10544  addpiord  10775  mulpiord  10776  pinq  10818  nqereu  10820  addpipq  10828  addpqnq  10829  mulpipq  10831  mulpqnq  10832  ordpipq  10833  recmulnq  10855  dmrecnq  10859  enreceq  10957  addsrpr  10966  mulsrpr  10967  0r  10971  1sr  10972  m1r  10973  addclsr  10974  mulclsr  10975  axaddf  11036  xrlenlt  11177  uzrdgfni  13865  swrdval  14551  ruclem6  16144  eucalgf  16494  eucalg  16498  qnumdenbi  16655  setscom  17091  strfv2d  17112  setsid  17118  imasaddfnlem  17432  imasaddflem  17434  imasvscafn  17441  imasvscaval  17442  funcpropd  17809  fucco  17872  catcxpccl  18113  curf1cl  18134  curf2cl  18137  curfcl  18138  uncfcurf  18145  diag2  18151  curf2ndf  18153  joindmss  18283  meetdmss  18297  latlem  18343  latjcom  18353  latmcom  18369  efgmf  19625  efglem  19628  vrgpf  19680  vrgpinv  19681  frgpuplem  19684  frgpup2  19688  frgpnabllem1  19785  gsumxp2  19892  rhmsubclem2  20601  pzriprnglem10  21427  mamudi  22318  mamudir  22319  mamuvs1  22320  mamuvs2  22321  matsubgcell  22349  matvscacell  22351  pmatcoe1fsupp  22616  txbas  23482  txcls  23519  upxp  23538  uptx  23540  txtube  23555  txcmplem1  23556  txlm  23563  tx1stc  23565  txkgen  23567  cnmpt21  23586  txswaphmeolem  23719  txswaphmeo  23720  clssubg  24024  qustgplem  24036  comet  24428  txmetcnp  24462  metustsym  24470  nrmmetd  24489  isngp3  24513  ngpds  24519  qtopbaslem  24673  cnmetdval  24685  remetdval  24704  tgqioo  24715  bndth  24884  htpyco2  24905  phtpyco2  24916  ovolicc1  25444  ioorf  25501  ioorcl  25505  itg1addlem4  25627  dvcnp2  25848  dvcnp2OLD  25849  dvef  25911  lhop1lem  25945  taylthlem2  26309  taylthlem2OLD  26310  addsqnreup  27381  addsfo  27926  subsfo  28005  noseqrdgfn  28236  brcgr  28878  ex-fpar  30442  imsdval  30666  sspval  30703  opreu2reuALT  32456  2ndimaxp  32628  ofoprabco  32646  f1od2  32702  qtophaus  33849  mbfmco2  34278  eulerpartlemgh  34391  afsval  34684  erdszelem9  35243  cvmlift2lem1  35346  cvmlift2lem9  35355  cvmlift2lem12  35358  cvmlift2lem13  35359  cvmliftphtlem  35361  goel  35391  goelel3xp  35392  sat1el2xp  35423  fmla0xp  35427  prv1n  35475  msubco  35575  msubff1  35600  mvhf  35602  msubvrs  35604  fvtransport  36076  colinearex  36104  bj-idres  37204  icoreunrn  37403  relowlpssretop  37408  curf  37648  finixpnum  37655  poimirlem15  37685  poimirlem25  37695  poimirlem26  37696  poimirlem27  37697  heicant  37705  mblfinlem1  37707  mblfinlem2  37708  ftc1anc  37751  opropabco  37774  heiborlem5  37865  dvhelvbasei  41197  dvhopvadd  41202  dvhvaddcl  41204  dvhopvsca  41211  dvhvscacl  41212  dvhgrp  41216  dvhopclN  41222  dvhopaddN  41223  dvhopspN  41224  dib1dim2  41277  diblss  41279  diclspsn  41303  dih1dimatlem  41438  hoicvr  46656  hoicvrrex  46664  ovnsubaddlem1  46678  ovnhoilem1  46709  ovnlecvr2  46718  opnvonmbllem1  46740  ovolval4lem2  46758  fnotaovb  47308  aovmpt4g  47311  rngccoALTV  48381  rhmsubcALTVlem2  48392  ringccoALTV  48415  rrx2plordisom  48834