Theorem opelxpi 5668

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

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

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5165  df-xp 5637

This theorem is referenced by:  opelxpii  5669  opelxpd  5670  opelvv  5671  opelvvg  5672  opbrop  5728  elsnxp  6252  reuop  6254  fnbrfvb2  6898  ov3  7532  ovres  7535  fovcdm  7539  fnovrn  7544  ovima0  7548  ovconst2  7549  el2xptp0  7994  opiota  8017  fimaproj  8091  xpord2pred  8101  seqomlem2  8396  brdifun  8678  ecopqsi  8721  brecop  8760  eceqoveq  8772  xpcomco  9008  djulcl  9839  djurcl  9840  djulf1o  9841  djurf1o  9842  djuun  9855  isfin4p1  10244  axdc4lem  10384  canthp1lem2  10582  addpiord  10813  mulpiord  10814  pinq  10856  nqereu  10858  addpipq  10866  addpqnq  10867  mulpipq  10869  mulpqnq  10870  ordpipq  10871  recmulnq  10893  dmrecnq  10897  enreceq  10995  addsrpr  11004  mulsrpr  11005  0r  11009  1sr  11010  m1r  11011  addclsr  11012  mulclsr  11013  axaddf  11074  xrlenlt  11215  uzrdgfni  13899  swrdval  14584  ruclem6  16179  eucalgf  16529  eucalg  16533  qnumdenbi  16690  setscom  17126  strfv2d  17147  setsid  17153  imasaddfnlem  17467  imasaddflem  17469  imasvscafn  17476  imasvscaval  17477  funcpropd  17844  fucco  17907  catcxpccl  18148  curf1cl  18169  curf2cl  18172  curfcl  18173  uncfcurf  18180  diag2  18186  curf2ndf  18188  joindmss  18318  meetdmss  18332  latlem  18378  latjcom  18388  latmcom  18404  efgmf  19627  efglem  19630  vrgpf  19682  vrgpinv  19683  frgpuplem  19686  frgpup2  19690  frgpnabllem1  19787  gsumxp2  19894  rhmsubclem2  20606  pzriprnglem10  21432  mamudi  22323  mamudir  22324  mamuvs1  22325  mamuvs2  22326  matsubgcell  22354  matvscacell  22356  pmatcoe1fsupp  22621  txbas  23487  txcls  23524  upxp  23543  uptx  23545  txtube  23560  txcmplem1  23561  txlm  23568  tx1stc  23570  txkgen  23572  cnmpt21  23591  txswaphmeolem  23724  txswaphmeo  23725  clssubg  24029  qustgplem  24041  comet  24434  txmetcnp  24468  metustsym  24476  nrmmetd  24495  isngp3  24519  ngpds  24525  qtopbaslem  24679  cnmetdval  24691  remetdval  24710  tgqioo  24721  bndth  24890  htpyco2  24911  phtpyco2  24922  ovolicc1  25450  ioorf  25507  ioorcl  25511  itg1addlem4  25633  dvcnp2  25854  dvcnp2OLD  25855  dvef  25917  lhop1lem  25951  taylthlem2  26315  taylthlem2OLD  26316  addsqnreup  27387  addsfo  27930  subsfo  28009  noseqrdgfn  28240  brcgr  28880  ex-fpar  30441  imsdval  30665  sspval  30702  opreu2reuALT  32456  2ndimaxp  32620  ofoprabco  32638  f1od2  32694  qtophaus  33819  mbfmco2  34249  eulerpartlemgh  34362  afsval  34655  erdszelem9  35179  cvmlift2lem1  35282  cvmlift2lem9  35291  cvmlift2lem12  35294  cvmlift2lem13  35295  cvmliftphtlem  35297  goel  35327  goelel3xp  35328  sat1el2xp  35359  fmla0xp  35363  prv1n  35411  msubco  35511  msubff1  35536  mvhf  35538  msubvrs  35540  fvtransport  36013  colinearex  36041  bj-idres  37141  icoreunrn  37340  relowlpssretop  37345  curf  37585  finixpnum  37592  poimirlem15  37622  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  heicant  37642  mblfinlem1  37644  mblfinlem2  37645  ftc1anc  37688  opropabco  37711  heiborlem5  37802  dvhelvbasei  41075  dvhopvadd  41080  dvhvaddcl  41082  dvhopvsca  41089  dvhvscacl  41090  dvhgrp  41094  dvhopclN  41100  dvhopaddN  41101  dvhopspN  41102  dib1dim2  41155  diblss  41157  diclspsn  41181  dih1dimatlem  41316  hoicvr  46539  hoicvrrex  46547  ovnsubaddlem1  46561  ovnhoilem1  46592  ovnlecvr2  46601  opnvonmbllem1  46623  ovolval4lem2  46641  fnotaovb  47192  aovmpt4g  47195  rngccoALTV  48252  rhmsubcALTVlem2  48263  ringccoALTV  48286  rrx2plordisom  48705