Theorem opelxpi 5687

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ⟨cop 4589   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-opab 5167  df-xp 5656

This theorem is used by:  opelxpii  5688  opelxpd  5689  opelvv  5690  opelvvg  5691  opbrop  5748  elsnxp  6294  reuop  6296  fnbrfvb2  6940  ov3  7583  ovres  7586  fovcdm  7591  fnovrn  7596  ovima0  7600  ovconst2  7601  el2xptp0  8047  opiota  8070  fimaproj  8152  xpord2pred  8162  seqomlem2  8461  brdifun  8748  ecopqsi  8791  brecop  8831  eceqoveq  8843  curf  8890  xpcomco  9086  djulcl  9991  djurcl  9992  djulf1o  9993  djurf1o  9994  djuun  10007  isfin4p1  10393  axdc4lem  10533  canthp1lem2  10738  addpiord  10969  mulpiord  10970  pinq  11012  nqereu  11014  addpipq  11022  addpqnq  11023  mulpipq  11025  mulpqnq  11026  ordpipq  11027  recmulnq  11049  dmrecnq  11053  enreceq  11151  addsrpr  11160  mulsrpr  11161  0r  11165  1sr  11166  m1r  11167  addclsr  11168  mulclsr  11169  axaddf  11230  xrlenlt  11374  uzrdgfni  14101  swrdval  14791  ruclem6  16403  eucalgf  16758  eucalg  16762  qnumdenbi  16920  setscom  17358  strfv2d  17379  setsid  17385  imasaddfnlem  17700  imasaddflem  17702  imasvscafn  17709  imasvscaval  17710  funcpropd  18077  fucco  18140  catcxpccl  18381  curf1cl  18402  curf2cl  18405  curfcl  18406  uncfcurf  18413  diag2  18419  curf2ndf  18421  joindmss  18551  meetdmss  18565  latlem  18611  latjcom  18621  latmcom  18637  mgmn0plusgplusf  18828  efgmf  19927  efglem  19930  vrgpf  19982  vrgpinv  19983  frgpuplem  19986  frgpup2  19990  frgpnabllem1  20087  gsumxp2  20194  rhmsubclem2  20938  pzriprnglem10  21796  mamudi  22718  mamudir  22719  mamuvs1  22720  mamuvs2  22721  matsubgcell  22749  matvscacell  22751  pmatcoe1fsupp  23019  txbas  23886  txcls  23923  upxp  23942  uptx  23944  txtube  23959  txcmplem1  23960  txlm  23967  tx1stc  23969  txkgen  23971  cnmpt21  23990  txswaphmeolem  24123  txswaphmeo  24124  clssubg  24428  qustgplem  24440  comet  24832  txmetcnp  24866  metustsym  24874  nrmmetd  24893  isngp3  24917  ngpds  24923  qtopbaslem  25077  cnmetdval  25089  remetdval  25108  tgqioo  25119  bndth  25279  htpyco2  25300  phtpyco2  25311  ovolicc1  25837  ioorf  25894  ioorcl  25898  itg1addlem4  26020  dvcnp2  26240  dvef  26300  lhop1lem  26333  taylthlem2  26701  addsqnreup  27770  addsfo  28369  subsfo  28451  noseqrdgfn  28692  brcgr  29478  ex-fpar  31063  imsdval  31288  sspval  31325  opreu2reuALT  33073  2ndimaxp  33240  ofoprabco  33258  f1od2  33311  qtophaus  34468  mbfmco2  34897  eulerpartlemgh  35010  afsval  35303  erdszelem9  35964  cvmlift2lem1  36067  cvmlift2lem9  36076  cvmlift2lem12  36079  cvmlift2lem13  36080  cvmliftphtlem  36082  goel  36112  goelel3xp  36113  sat1el2xp  36144  fmla0xp  36148  prv1n  36196  msubco  36296  msubff1  36321  mvhf  36323  msubvrs  36325  fvtransport  36797  colinearex  36825  nmulprop  36939  bj-idres  38082  icoreunrn  38283  relowlpssretop  38288  finixpnum  38529  poimirlem15  38554  poimirlem25  38564  poimirlem26  38565  poimirlem27  38566  heicant  38574  mblfinlem1  38576  mblfinlem2  38577  ftc1anc  38620  opropabco  38659  heiborlem5  38750  dvhelvbasei  42146  dvhopvadd  42151  dvhvaddcl  42153  dvhopvsca  42160  dvhvscacl  42161  dvhgrp  42165  dvhopclN  42171  dvhopaddN  42172  dvhopspN  42173  dib1dim2  42226  diblss  42228  diclspsn  42252  dih1dimatlem  42387  hoicvrrex  47566  ovnsubaddlem1  47580  ovnhoilem1  47611  ovnlecvr2  47620  opnvonmbllem1  47642  ovolval4lem2  47660  fnotaovb  48268  aovmpt4g  48271  rngccoALTV  49368  rhmsubcALTVlem2  49379  ringccoALTV  49402  rrx2plordisom  49835