Theorem opelxpi 5696

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ⟨cop 4593   × cxp 5657

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 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5172  df-xp 5665

This theorem is used by:  opelxpii  5697  opelxpd  5698  opelvv  5699  opelvvg  5700  opbrop  5757  elsnxp  6293  reuop  6295  fnbrfvb2  6937  ov3  7580  ovres  7583  fovcdm  7588  fnovrn  7593  ovima0  7597  ovconst2  7598  el2xptp0  8037  opiota  8060  fimaproj  8137  xpord2pred  8147  seqomlem2  8444  brdifun  8731  ecopqsi  8774  brecop  8814  eceqoveq  8826  curf  8873  xpcomco  9069  djulcl  9919  djurcl  9920  djulf1o  9921  djurf1o  9922  djuun  9935  isfin4p1  10321  axdc4lem  10461  canthp1lem2  10666  addpiord  10897  mulpiord  10898  pinq  10940  nqereu  10942  addpipq  10950  addpqnq  10951  mulpipq  10953  mulpqnq  10954  ordpipq  10955  recmulnq  10977  dmrecnq  10981  enreceq  11079  addsrpr  11088  mulsrpr  11089  0r  11093  1sr  11094  m1r  11095  addclsr  11096  mulclsr  11097  axaddf  11158  xrlenlt  11302  uzrdgfni  14026  swrdval  14715  ruclem6  16329  eucalgf  16679  eucalg  16683  qnumdenbi  16841  setscom  17278  strfv2d  17299  setsid  17305  imasaddfnlem  17620  imasaddflem  17622  imasvscafn  17629  imasvscaval  17630  funcpropd  17997  fucco  18060  catcxpccl  18301  curf1cl  18322  curf2cl  18325  curfcl  18326  uncfcurf  18333  diag2  18339  curf2ndf  18341  joindmss  18471  meetdmss  18485  latlem  18531  latjcom  18541  latmcom  18557  mgmn0plusgplusf  18748  efgmf  19846  efglem  19849  vrgpf  19901  vrgpinv  19902  frgpuplem  19905  frgpup2  19909  frgpnabllem1  20006  gsumxp2  20113  rhmsubclem2  20854  pzriprnglem10  21709  mamudi  22631  mamudir  22632  mamuvs1  22633  mamuvs2  22634  matsubgcell  22662  matvscacell  22664  pmatcoe1fsupp  22932  txbas  23799  txcls  23836  upxp  23855  uptx  23857  txtube  23872  txcmplem1  23873  txlm  23880  tx1stc  23882  txkgen  23884  cnmpt21  23903  txswaphmeolem  24036  txswaphmeo  24037  clssubg  24341  qustgplem  24353  comet  24745  txmetcnp  24779  metustsym  24787  nrmmetd  24806  isngp3  24830  ngpds  24836  qtopbaslem  24990  cnmetdval  25002  remetdval  25021  tgqioo  25032  bndth  25192  htpyco2  25213  phtpyco2  25224  ovolicc1  25750  ioorf  25807  ioorcl  25811  itg1addlem4  25933  dvcnp2  26154  dvef  26214  lhop1lem  26247  taylthlem2  26617  addsqnreup  27687  addsfo  28256  subsfo  28338  noseqrdgfn  28579  brcgr  29365  ex-fpar  30950  imsdval  31175  sspval  31212  opreu2reuALT  32960  2ndimaxp  33127  ofoprabco  33145  f1od2  33198  qtophaus  34354  mbfmco2  34784  eulerpartlemgh  34897  afsval  35190  erdszelem9  35786  cvmlift2lem1  35889  cvmlift2lem9  35898  cvmlift2lem12  35901  cvmlift2lem13  35902  cvmliftphtlem  35904  goel  35934  goelel3xp  35935  sat1el2xp  35966  fmla0xp  35970  prv1n  36018  msubco  36118  msubff1  36143  mvhf  36145  msubvrs  36147  fvtransport  36620  colinearex  36648  nmulprop  36778  bj-idres  37920  icoreunrn  38121  relowlpssretop  38126  finixpnum  38367  poimirlem15  38392  poimirlem25  38402  poimirlem26  38403  poimirlem27  38404  heicant  38412  mblfinlem1  38414  mblfinlem2  38415  ftc1anc  38458  opropabco  38482  heiborlem5  38573  dvhelvbasei  41969  dvhopvadd  41974  dvhvaddcl  41976  dvhopvsca  41983  dvhvscacl  41984  dvhgrp  41988  dvhopclN  41994  dvhopaddN  41995  dvhopspN  41996  dib1dim2  42049  diblss  42051  diclspsn  42075  dih1dimatlem  42210  hoicvrrex  47392  ovnsubaddlem1  47406  ovnhoilem1  47437  ovnlecvr2  47446  opnvonmbllem1  47468  ovolval4lem2  47486  fnotaovb  48094  aovmpt4g  48097  rngccoALTV  49194  rhmsubcALTVlem2  49205  ringccoALTV  49228  rrx2plordisom  49661