Theorem opelxpi 5591

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  ⟨cop 4572   × cxp 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-opab 5128  df-xp 5560

This theorem is referenced by:  opelxpd  5592  opelvv  5593  opelvvg  5594  opbrop  5647  elsnxp  6141  reuop  6143  fnbrfvb2  6721  ov3  7310  ovres  7313  fovrn  7317  fnovrn  7322  ovima0  7326  ovconst2  7327  el2xptp0  7735  opiota  7756  fimaproj  7828  seqomlem2  8086  brdifun  8317  ecopqsi  8353  brecop  8389  eceqoveq  8401  xpcomco  8606  djulcl  9338  djurcl  9339  djulf1o  9340  djurf1o  9341  djuun  9354  isfin4p1  9736  axdc4lem  9876  canthp1lem2  10074  addpiord  10305  mulpiord  10306  pinq  10348  nqereu  10350  addpipq  10358  addpqnq  10359  mulpipq  10361  mulpqnq  10362  ordpipq  10363  recmulnq  10385  dmrecnq  10389  enreceq  10487  addsrpr  10496  mulsrpr  10497  0r  10501  1sr  10502  m1r  10503  addclsr  10504  mulclsr  10505  axaddf  10566  xrlenlt  10705  uzrdgfni  13325  swrdval  14004  ruclem6  15587  eucalgf  15926  eucalg  15930  qnumdenbi  16083  setscom  16526  strfv2d  16528  setsid  16537  imasaddfnlem  16800  imasaddflem  16802  imasvscafn  16809  imasvscaval  16810  funcpropd  17169  fucco  17231  catcxpccl  17456  curf1cl  17477  curf2cl  17480  curfcl  17481  uncfcurf  17488  diag2  17494  curf2ndf  17496  joindmss  17616  meetdmss  17630  latlem  17658  latjcom  17668  latmcom  17684  efgmf  18838  efglem  18841  vrgpf  18893  vrgpinv  18894  frgpuplem  18897  frgpup2  18901  frgpnabllem1  18992  gsumxp2  19099  mamudi  21011  mamudir  21012  mamuvs1  21013  mamuvs2  21014  matsubgcell  21042  matvscacell  21044  pmatcoe1fsupp  21308  txbas  22174  txcls  22211  upxp  22230  uptx  22232  txtube  22247  txcmplem1  22248  txlm  22255  tx1stc  22257  txkgen  22259  cnmpt21  22278  txswaphmeolem  22411  txswaphmeo  22412  clssubg  22716  qustgplem  22728  comet  23122  txmetcnp  23156  metustsym  23164  nrmmetd  23183  isngp3  23206  ngpds  23212  qtopbaslem  23366  cnmetdval  23378  remetdval  23396  tgqioo  23407  bndth  23561  htpyco2  23582  phtpyco2  23593  ovolicc1  24116  ioorf  24173  ioorcl  24177  itg1addlem4  24299  dvcnp2  24516  dvef  24576  lhop1lem  24609  taylthlem2  24961  addsqnreup  26018  brcgr  26685  ex-fpar  28240  imsdval  28462  sspval  28499  opreu2reuALT  30239  ofoprabco  30408  f1od2  30456  qtophaus  31100  mbfmco2  31523  eulerpartlemgh  31636  afsval  31942  erdszelem9  32446  cvmlift2lem1  32549  cvmlift2lem9  32558  cvmlift2lem12  32561  cvmlift2lem13  32562  cvmliftphtlem  32564  goel  32594  goelel3xp  32595  sat1el2xp  32626  fmla0xp  32630  prv1n  32678  msubco  32778  msubff1  32803  mvhf  32805  msubvrs  32807  fvtransport  33493  colinearex  33521  bj-idres  34451  icoreunrn  34639  relowlpssretop  34644  curf  34869  finixpnum  34876  poimirlem3  34894  poimirlem4  34895  poimirlem15  34906  poimirlem17  34908  poimirlem20  34911  poimirlem25  34916  poimirlem26  34917  poimirlem27  34918  heicant  34926  mblfinlem1  34928  mblfinlem2  34929  ftc1anc  34974  opropabco  34998  heiborlem5  35092  dvhelvbasei  38223  dvhopvadd  38228  dvhvaddcl  38230  dvhopvsca  38237  dvhvscacl  38238  dvhgrp  38242  dvhopclN  38248  dvhopaddN  38249  dvhopspN  38250  dib1dim2  38303  diblss  38305  diclspsn  38329  dih1dimatlem  38464  opelxpii  39115  hoicvr  42829  hoicvrrex  42837  ovnsubaddlem1  42851  ovnhoilem1  42882  ovnlecvr2  42891  opnvonmbllem1  42913  ovolval4lem2  42931  fnotaovb  43396  aovmpt4g  43399  rngccoALTV  44258  ringccoALTV  44321  rhmsubclem2  44357  rhmsubcALTVlem2  44375  rrx2plordisom  44709