Theorem opelxpi 5713

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ⟨cop 4634   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-opab 5211  df-xp 5682

This theorem is referenced by:  opelxpii  5714  opelxpd  5715  opelvv  5716  opelvvg  5717  opbrop  5773  elsnxp  6290  reuop  6292  fnbrfvb2  6948  ov3  7572  ovres  7575  fovcdm  7579  fnovrn  7584  ovima0  7588  ovconst2  7589  el2xptp0  8024  opiota  8047  fimaproj  8123  xpord2pred  8133  seqomlem2  8453  brdifun  8734  ecopqsi  8770  brecop  8806  eceqoveq  8818  xpcomco  9064  djulcl  9907  djurcl  9908  djulf1o  9909  djurf1o  9910  djuun  9923  isfin4p1  10312  axdc4lem  10452  canthp1lem2  10650  addpiord  10881  mulpiord  10882  pinq  10924  nqereu  10926  addpipq  10934  addpqnq  10935  mulpipq  10937  mulpqnq  10938  ordpipq  10939  recmulnq  10961  dmrecnq  10965  enreceq  11063  addsrpr  11072  mulsrpr  11073  0r  11077  1sr  11078  m1r  11079  addclsr  11080  mulclsr  11081  axaddf  11142  xrlenlt  11283  uzrdgfni  13927  swrdval  14597  ruclem6  16182  eucalgf  16524  eucalg  16528  qnumdenbi  16684  setscom  17117  strfv2d  17139  setsid  17145  imasaddfnlem  17478  imasaddflem  17480  imasvscafn  17487  imasvscaval  17488  funcpropd  17855  fucco  17919  catcxpccl  18163  catcxpcclOLD  18164  curf1cl  18185  curf2cl  18188  curfcl  18189  uncfcurf  18196  diag2  18202  curf2ndf  18204  joindmss  18336  meetdmss  18350  latlem  18394  latjcom  18404  latmcom  18420  efgmf  19622  efglem  19625  vrgpf  19677  vrgpinv  19678  frgpuplem  19681  frgpup2  19685  frgpnabllem1  19782  gsumxp2  19889  pzriprnglem10  21259  mamudi  22123  mamudir  22124  mamuvs1  22125  mamuvs2  22126  matsubgcell  22156  matvscacell  22158  pmatcoe1fsupp  22423  txbas  23291  txcls  23328  upxp  23347  uptx  23349  txtube  23364  txcmplem1  23365  txlm  23372  tx1stc  23374  txkgen  23376  cnmpt21  23395  txswaphmeolem  23528  txswaphmeo  23529  clssubg  23833  qustgplem  23845  comet  24242  txmetcnp  24276  metustsym  24284  nrmmetd  24303  isngp3  24327  ngpds  24333  qtopbaslem  24495  cnmetdval  24507  remetdval  24525  tgqioo  24536  bndth  24698  htpyco2  24719  phtpyco2  24730  ovolicc1  25257  ioorf  25314  ioorcl  25318  itg1addlem4  25440  itg1addlem4OLD  25441  dvcnp2  25661  dvef  25721  lhop1lem  25754  taylthlem2  26110  addsqnreup  27170  addsfo  27693  brcgr  28413  ex-fpar  29970  imsdval  30194  sspval  30231  opreu2reuALT  31972  2ndimaxp  32127  ofoprabco  32144  f1od2  32201  qtophaus  33102  mbfmco2  33550  eulerpartlemgh  33663  afsval  33969  erdszelem9  34476  cvmlift2lem1  34579  cvmlift2lem9  34588  cvmlift2lem12  34591  cvmlift2lem13  34592  cvmliftphtlem  34594  goel  34624  goelel3xp  34625  sat1el2xp  34656  fmla0xp  34660  prv1n  34708  msubco  34808  msubff1  34833  mvhf  34835  msubvrs  34837  fvtransport  35296  colinearex  35324  gg-dvcnp2  35460  bj-idres  36344  icoreunrn  36543  relowlpssretop  36548  curf  36769  finixpnum  36776  poimirlem15  36806  poimirlem25  36816  poimirlem26  36817  poimirlem27  36818  heicant  36826  mblfinlem1  36828  mblfinlem2  36829  ftc1anc  36872  opropabco  36895  heiborlem5  36986  dvhelvbasei  40262  dvhopvadd  40267  dvhvaddcl  40269  dvhopvsca  40276  dvhvscacl  40277  dvhgrp  40281  dvhopclN  40287  dvhopaddN  40288  dvhopspN  40289  dib1dim2  40342  diblss  40344  diclspsn  40368  dih1dimatlem  40503  hoicvr  45563  hoicvrrex  45571  ovnsubaddlem1  45585  ovnhoilem1  45616  ovnlecvr2  45625  opnvonmbllem1  45647  ovolval4lem2  45665  fnotaovb  46205  aovmpt4g  46208  rngccoALTV  46975  ringccoALTV  47038  rhmsubclem2  47074  rhmsubcALTVlem2  47092  rrx2plordisom  47497