Theorem opelxpi 5656

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

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

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-opab 5155  df-xp 5625

This theorem is referenced by:  opelxpii  5657  opelxpd  5658  opelvv  5659  opelvvg  5660  opbrop  5717  elsnxp  6239  reuop  6241  fnbrfvb2  6878  ov3  7512  ovres  7515  fovcdm  7519  fnovrn  7524  ovima0  7528  ovconst2  7529  el2xptp0  7971  opiota  7994  fimaproj  8068  xpord2pred  8078  seqomlem2  8373  brdifun  8655  ecopqsi  8698  brecop  8737  eceqoveq  8749  xpcomco  8984  djulcl  9806  djurcl  9807  djulf1o  9808  djurf1o  9809  djuun  9822  isfin4p1  10209  axdc4lem  10349  canthp1lem2  10547  addpiord  10778  mulpiord  10779  pinq  10821  nqereu  10823  addpipq  10831  addpqnq  10832  mulpipq  10834  mulpqnq  10835  ordpipq  10836  recmulnq  10858  dmrecnq  10862  enreceq  10960  addsrpr  10969  mulsrpr  10970  0r  10974  1sr  10975  m1r  10976  addclsr  10977  mulclsr  10978  axaddf  11039  xrlenlt  11180  uzrdgfni  13865  swrdval  14550  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  19592  efglem  19595  vrgpf  19647  vrgpinv  19648  frgpuplem  19651  frgpup2  19655  frgpnabllem1  19752  gsumxp2  19859  rhmsubclem2  20571  pzriprnglem10  21397  mamudi  22288  mamudir  22289  mamuvs1  22290  mamuvs2  22291  matsubgcell  22319  matvscacell  22321  pmatcoe1fsupp  22586  txbas  23452  txcls  23489  upxp  23508  uptx  23510  txtube  23525  txcmplem1  23526  txlm  23533  tx1stc  23535  txkgen  23537  cnmpt21  23556  txswaphmeolem  23689  txswaphmeo  23690  clssubg  23994  qustgplem  24006  comet  24399  txmetcnp  24433  metustsym  24441  nrmmetd  24460  isngp3  24484  ngpds  24490  qtopbaslem  24644  cnmetdval  24656  remetdval  24675  tgqioo  24686  bndth  24855  htpyco2  24876  phtpyco2  24887  ovolicc1  25415  ioorf  25472  ioorcl  25476  itg1addlem4  25598  dvcnp2  25819  dvcnp2OLD  25820  dvef  25882  lhop1lem  25916  taylthlem2  26280  taylthlem2OLD  26281  addsqnreup  27352  addsfo  27895  subsfo  27974  noseqrdgfn  28205  brcgr  28845  ex-fpar  30406  imsdval  30630  sspval  30667  opreu2reuALT  32421  2ndimaxp  32590  ofoprabco  32608  f1od2  32664  qtophaus  33809  mbfmco2  34239  eulerpartlemgh  34352  afsval  34645  erdszelem9  35182  cvmlift2lem1  35285  cvmlift2lem9  35294  cvmlift2lem12  35297  cvmlift2lem13  35298  cvmliftphtlem  35300  goel  35330  goelel3xp  35331  sat1el2xp  35362  fmla0xp  35366  prv1n  35414  msubco  35514  msubff1  35539  mvhf  35541  msubvrs  35543  fvtransport  36016  colinearex  36044  bj-idres  37144  icoreunrn  37343  relowlpssretop  37348  curf  37588  finixpnum  37595  poimirlem15  37625  poimirlem25  37635  poimirlem26  37636  poimirlem27  37637  heicant  37645  mblfinlem1  37647  mblfinlem2  37648  ftc1anc  37691  opropabco  37714  heiborlem5  37805  dvhelvbasei  41077  dvhopvadd  41082  dvhvaddcl  41084  dvhopvsca  41091  dvhvscacl  41092  dvhgrp  41096  dvhopclN  41102  dvhopaddN  41103  dvhopspN  41104  dib1dim2  41157  diblss  41159  diclspsn  41183  dih1dimatlem  41318  hoicvr  46539  hoicvrrex  46547  ovnsubaddlem1  46561  ovnhoilem1  46592  ovnlecvr2  46601  opnvonmbllem1  46623  ovolval4lem2  46641  fnotaovb  47192  aovmpt4g  47195  rngccoALTV  48265  rhmsubcALTVlem2  48276  ringccoALTV  48299  rrx2plordisom  48718