Theorem opelxpi 5675

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ⟨cop 4595   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-xp 5644

This theorem is referenced by:  opelxpii  5676  opelxpd  5677  opelvv  5678  opelvvg  5679  opbrop  5736  elsnxp  6264  reuop  6266  fnbrfvb2  6916  ov3  7552  ovres  7555  fovcdm  7559  fnovrn  7564  ovima0  7568  ovconst2  7569  el2xptp0  8015  opiota  8038  fimaproj  8114  xpord2pred  8124  seqomlem2  8419  brdifun  8701  ecopqsi  8744  brecop  8783  eceqoveq  8795  xpcomco  9031  djulcl  9863  djurcl  9864  djulf1o  9865  djurf1o  9866  djuun  9879  isfin4p1  10268  axdc4lem  10408  canthp1lem2  10606  addpiord  10837  mulpiord  10838  pinq  10880  nqereu  10882  addpipq  10890  addpqnq  10891  mulpipq  10893  mulpqnq  10894  ordpipq  10895  recmulnq  10917  dmrecnq  10921  enreceq  11019  addsrpr  11028  mulsrpr  11029  0r  11033  1sr  11034  m1r  11035  addclsr  11036  mulclsr  11037  axaddf  11098  xrlenlt  11239  uzrdgfni  13923  swrdval  14608  ruclem6  16203  eucalgf  16553  eucalg  16557  qnumdenbi  16714  setscom  17150  strfv2d  17171  setsid  17177  imasaddfnlem  17491  imasaddflem  17493  imasvscafn  17500  imasvscaval  17501  funcpropd  17864  fucco  17927  catcxpccl  18168  curf1cl  18189  curf2cl  18192  curfcl  18193  uncfcurf  18200  diag2  18206  curf2ndf  18208  joindmss  18338  meetdmss  18352  latlem  18396  latjcom  18406  latmcom  18422  efgmf  19643  efglem  19646  vrgpf  19698  vrgpinv  19699  frgpuplem  19702  frgpup2  19706  frgpnabllem1  19803  gsumxp2  19910  rhmsubclem2  20595  pzriprnglem10  21400  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  matsubgcell  22321  matvscacell  22323  pmatcoe1fsupp  22588  txbas  23454  txcls  23491  upxp  23510  uptx  23512  txtube  23527  txcmplem1  23528  txlm  23535  tx1stc  23537  txkgen  23539  cnmpt21  23558  txswaphmeolem  23691  txswaphmeo  23692  clssubg  23996  qustgplem  24008  comet  24401  txmetcnp  24435  metustsym  24443  nrmmetd  24462  isngp3  24486  ngpds  24492  qtopbaslem  24646  cnmetdval  24658  remetdval  24677  tgqioo  24688  bndth  24857  htpyco2  24878  phtpyco2  24889  ovolicc1  25417  ioorf  25474  ioorcl  25478  itg1addlem4  25600  dvcnp2  25821  dvcnp2OLD  25822  dvef  25884  lhop1lem  25918  taylthlem2  26282  taylthlem2OLD  26283  addsqnreup  27354  addsfo  27890  subsfo  27969  noseqrdgfn  28200  brcgr  28827  ex-fpar  30391  imsdval  30615  sspval  30652  opreu2reuALT  32406  2ndimaxp  32570  ofoprabco  32588  f1od2  32644  qtophaus  33826  mbfmco2  34256  eulerpartlemgh  34369  afsval  34662  erdszelem9  35186  cvmlift2lem1  35289  cvmlift2lem9  35298  cvmlift2lem12  35301  cvmlift2lem13  35302  cvmliftphtlem  35304  goel  35334  goelel3xp  35335  sat1el2xp  35366  fmla0xp  35370  prv1n  35418  msubco  35518  msubff1  35543  mvhf  35545  msubvrs  35547  fvtransport  36020  colinearex  36048  bj-idres  37148  icoreunrn  37347  relowlpssretop  37352  curf  37592  finixpnum  37599  poimirlem15  37629  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  heicant  37649  mblfinlem1  37651  mblfinlem2  37652  ftc1anc  37695  opropabco  37718  heiborlem5  37809  dvhelvbasei  41082  dvhopvadd  41087  dvhvaddcl  41089  dvhopvsca  41096  dvhvscacl  41097  dvhgrp  41101  dvhopclN  41107  dvhopaddN  41108  dvhopspN  41109  dib1dim2  41162  diblss  41164  diclspsn  41188  dih1dimatlem  41323  hoicvr  46546  hoicvrrex  46554  ovnsubaddlem1  46568  ovnhoilem1  46599  ovnlecvr2  46608  opnvonmbllem1  46630  ovolval4lem2  46648  fnotaovb  47199  aovmpt4g  47202  rngccoALTV  48259  rhmsubcALTVlem2  48270  ringccoALTV  48293  rrx2plordisom  48712