Theorem opelxpi 5714

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ⟨cop 4635   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-opab 5212  df-xp 5683

This theorem is referenced by:  opelxpii  5715  opelxpd  5716  opelvv  5717  opelvvg  5718  opbrop  5774  elsnxp  6291  reuop  6293  fnbrfvb2  6949  ov3  7570  ovres  7573  fovcdm  7577  fnovrn  7582  ovima0  7586  ovconst2  7587  el2xptp0  8022  opiota  8045  fimaproj  8121  xpord2pred  8131  seqomlem2  8451  brdifun  8732  ecopqsi  8768  brecop  8804  eceqoveq  8816  xpcomco  9062  djulcl  9905  djurcl  9906  djulf1o  9907  djurf1o  9908  djuun  9921  isfin4p1  10310  axdc4lem  10450  canthp1lem2  10648  addpiord  10879  mulpiord  10880  pinq  10922  nqereu  10924  addpipq  10932  addpqnq  10933  mulpipq  10935  mulpqnq  10936  ordpipq  10937  recmulnq  10959  dmrecnq  10963  enreceq  11061  addsrpr  11070  mulsrpr  11071  0r  11075  1sr  11076  m1r  11077  addclsr  11078  mulclsr  11079  axaddf  11140  xrlenlt  11279  uzrdgfni  13923  swrdval  14593  ruclem6  16178  eucalgf  16520  eucalg  16524  qnumdenbi  16680  setscom  17113  strfv2d  17135  setsid  17141  imasaddfnlem  17474  imasaddflem  17476  imasvscafn  17483  imasvscaval  17484  funcpropd  17851  fucco  17915  catcxpccl  18159  catcxpcclOLD  18160  curf1cl  18181  curf2cl  18184  curfcl  18185  uncfcurf  18192  diag2  18198  curf2ndf  18200  joindmss  18332  meetdmss  18346  latlem  18390  latjcom  18400  latmcom  18416  efgmf  19581  efglem  19584  vrgpf  19636  vrgpinv  19637  frgpuplem  19640  frgpup2  19644  frgpnabllem1  19741  gsumxp2  19848  mamudi  21903  mamudir  21904  mamuvs1  21905  mamuvs2  21906  matsubgcell  21936  matvscacell  21938  pmatcoe1fsupp  22203  txbas  23071  txcls  23108  upxp  23127  uptx  23129  txtube  23144  txcmplem1  23145  txlm  23152  tx1stc  23154  txkgen  23156  cnmpt21  23175  txswaphmeolem  23308  txswaphmeo  23309  clssubg  23613  qustgplem  23625  comet  24022  txmetcnp  24056  metustsym  24064  nrmmetd  24083  isngp3  24107  ngpds  24113  qtopbaslem  24275  cnmetdval  24287  remetdval  24305  tgqioo  24316  bndth  24474  htpyco2  24495  phtpyco2  24506  ovolicc1  25033  ioorf  25090  ioorcl  25094  itg1addlem4  25216  itg1addlem4OLD  25217  dvcnp2  25437  dvef  25497  lhop1lem  25530  taylthlem2  25886  addsqnreup  26946  addsfo  27467  brcgr  28158  ex-fpar  29715  imsdval  29939  sspval  29976  opreu2reuALT  31717  2ndimaxp  31872  ofoprabco  31889  f1od2  31946  qtophaus  32816  mbfmco2  33264  eulerpartlemgh  33377  afsval  33683  erdszelem9  34190  cvmlift2lem1  34293  cvmlift2lem9  34302  cvmlift2lem12  34305  cvmlift2lem13  34306  cvmliftphtlem  34308  goel  34338  goelel3xp  34339  sat1el2xp  34370  fmla0xp  34374  prv1n  34422  msubco  34522  msubff1  34547  mvhf  34549  msubvrs  34551  fvtransport  35004  colinearex  35032  gg-dvcnp2  35174  bj-idres  36041  icoreunrn  36240  relowlpssretop  36245  curf  36466  finixpnum  36473  poimirlem15  36503  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  heicant  36523  mblfinlem1  36525  mblfinlem2  36526  ftc1anc  36569  opropabco  36592  heiborlem5  36683  dvhelvbasei  39959  dvhopvadd  39964  dvhvaddcl  39966  dvhopvsca  39973  dvhvscacl  39974  dvhgrp  39978  dvhopclN  39984  dvhopaddN  39985  dvhopspN  39986  dib1dim2  40039  diblss  40041  diclspsn  40065  dih1dimatlem  40200  hoicvr  45264  hoicvrrex  45272  ovnsubaddlem1  45286  ovnhoilem1  45317  ovnlecvr2  45326  opnvonmbllem1  45348  ovolval4lem2  45366  fnotaovb  45906  aovmpt4g  45909  pzriprnglem10  46814  rngccoALTV  46886  ringccoALTV  46949  rhmsubclem2  46985  rhmsubcALTVlem2  47003  rrx2plordisom  47409