Theorem opelxpi 5700

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ⟨cop 4597   × cxp 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5176  df-xp 5669

This theorem is used by:  opelxpii  5701  opelxpd  5702  opelvv  5703  opelvvg  5704  opbrop  5761  elsnxp  6297  reuop  6299  fnbrfvb2  6941  ov3  7583  ovres  7586  fovcdm  7591  fnovrn  7596  ovima0  7600  ovconst2  7601  el2xptp0  8040  opiota  8063  fimaproj  8138  xpord2pred  8148  seqomlem2  8445  brdifun  8732  ecopqsi  8775  brecop  8815  eceqoveq  8827  xpcomco  9063  djulcl  9913  djurcl  9914  djulf1o  9915  djurf1o  9916  djuun  9929  isfin4p1  10315  axdc4lem  10455  canthp1lem2  10658  addpiord  10889  mulpiord  10890  pinq  10932  nqereu  10934  addpipq  10942  addpqnq  10943  mulpipq  10945  mulpqnq  10946  ordpipq  10947  recmulnq  10969  dmrecnq  10973  enreceq  11071  addsrpr  11080  mulsrpr  11081  0r  11085  1sr  11086  m1r  11087  addclsr  11088  mulclsr  11089  axaddf  11150  xrlenlt  11294  uzrdgfni  14017  swrdval  14706  ruclem6  16318  eucalgf  16668  eucalg  16672  qnumdenbi  16830  setscom  17267  strfv2d  17288  setsid  17294  imasaddfnlem  17609  imasaddflem  17611  imasvscafn  17618  imasvscaval  17619  funcpropd  17986  fucco  18049  catcxpccl  18290  curf1cl  18311  curf2cl  18314  curfcl  18315  uncfcurf  18322  diag2  18328  curf2ndf  18330  joindmss  18460  meetdmss  18474  latlem  18520  latjcom  18530  latmcom  18546  mgmn0plusgplusf  18737  efgmf  19832  efglem  19835  vrgpf  19887  vrgpinv  19888  frgpuplem  19891  frgpup2  19895  frgpnabllem1  19992  gsumxp2  20099  rhmsubclem2  20840  pzriprnglem10  21695  mamudi  22615  mamudir  22616  mamuvs1  22617  mamuvs2  22618  matsubgcell  22646  matvscacell  22648  pmatcoe1fsupp  22913  txbas  23780  txcls  23817  upxp  23836  uptx  23838  txtube  23853  txcmplem1  23854  txlm  23861  tx1stc  23863  txkgen  23865  cnmpt21  23884  txswaphmeolem  24017  txswaphmeo  24018  clssubg  24322  qustgplem  24334  comet  24726  txmetcnp  24760  metustsym  24768  nrmmetd  24787  isngp3  24811  ngpds  24817  qtopbaslem  24971  cnmetdval  24983  remetdval  25002  tgqioo  25013  bndth  25173  htpyco2  25194  phtpyco2  25205  ovolicc1  25731  ioorf  25788  ioorcl  25792  itg1addlem4  25914  dvcnp2  26135  dvef  26195  lhop1lem  26228  taylthlem2  26593  addsqnreup  27663  addsfo  28232  subsfo  28314  noseqrdgfn  28555  brcgr  29310  ex-fpar  30889  imsdval  31114  sspval  31151  opreu2reuALT  32899  2ndimaxp  33067  ofoprabco  33085  f1od2  33139  qtophaus  34295  mbfmco2  34725  eulerpartlemgh  34838  afsval  35131  erdszelem9  35733  cvmlift2lem1  35836  cvmlift2lem9  35845  cvmlift2lem12  35848  cvmlift2lem13  35849  cvmliftphtlem  35851  goel  35881  goelel3xp  35882  sat1el2xp  35913  fmla0xp  35917  prv1n  35965  msubco  36065  msubff1  36090  mvhf  36092  msubvrs  36094  fvtransport  36566  colinearex  36594  nmulprop  36724  bj-idres  37866  icoreunrn  38067  relowlpssretop  38072  curf  38311  finixpnum  38318  poimirlem15  38348  poimirlem25  38358  poimirlem26  38359  poimirlem27  38360  heicant  38368  mblfinlem1  38370  mblfinlem2  38371  ftc1anc  38414  opropabco  38438  heiborlem5  38529  dvhelvbasei  41925  dvhopvadd  41930  dvhvaddcl  41932  dvhopvsca  41939  dvhvscacl  41940  dvhgrp  41944  dvhopclN  41950  dvhopaddN  41951  dvhopspN  41952  dib1dim2  42005  diblss  42007  diclspsn  42031  dih1dimatlem  42166  hoicvrrex  47348  ovnsubaddlem1  47362  ovnhoilem1  47393  ovnlecvr2  47402  opnvonmbllem1  47424  ovolval4lem2  47442  fnotaovb  48013  aovmpt4g  48016  rngccoALTV  49113  rhmsubcALTVlem2  49124  ringccoALTV  49147  rrx2plordisom  49580