Theorem opelxpi 5586

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

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

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 5195  ax-nul 5202  ax-pr 5321

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 4561  df-pr 4563  df-op 4567  df-opab 5121  df-xp 5555

This theorem is referenced by:  opelxpd  5587  opelvv  5588  opelvvg  5589  opbrop  5642  elsnxp  6136  reuop  6138  fnbrfvb2  6716  ov3  7305  ovres  7308  fovrn  7312  fnovrn  7317  ovima0  7321  ovconst2  7322  el2xptp0  7730  opiota  7751  fimaproj  7823  seqomlem2  8081  brdifun  8312  ecopqsi  8348  brecop  8384  eceqoveq  8396  xpcomco  8601  djulcl  9333  djurcl  9334  djulf1o  9335  djurf1o  9336  djuun  9349  isfin4p1  9731  axdc4lem  9871  canthp1lem2  10069  addpiord  10300  mulpiord  10301  pinq  10343  nqereu  10345  addpipq  10353  addpqnq  10354  mulpipq  10356  mulpqnq  10357  ordpipq  10358  recmulnq  10380  dmrecnq  10384  enreceq  10482  addsrpr  10491  mulsrpr  10492  0r  10496  1sr  10497  m1r  10498  addclsr  10499  mulclsr  10500  axaddf  10561  xrlenlt  10700  uzrdgfni  13320  swrdval  13999  ruclem6  15582  eucalgf  15921  eucalg  15925  qnumdenbi  16078  setscom  16521  strfv2d  16523  setsid  16532  imasaddfnlem  16795  imasaddflem  16797  imasvscafn  16804  imasvscaval  16805  funcpropd  17164  fucco  17226  catcxpccl  17451  curf1cl  17472  curf2cl  17475  curfcl  17476  uncfcurf  17483  diag2  17489  curf2ndf  17491  joindmss  17611  meetdmss  17625  latlem  17653  latjcom  17663  latmcom  17679  efgmf  18833  efglem  18836  vrgpf  18888  vrgpinv  18889  frgpuplem  18892  frgpup2  18896  frgpnabllem1  18987  gsumxp2  19094  mamudi  21006  mamudir  21007  mamuvs1  21008  mamuvs2  21009  matsubgcell  21037  matvscacell  21039  pmatcoe1fsupp  21303  txbas  22169  txcls  22206  upxp  22225  uptx  22227  txtube  22242  txcmplem1  22243  txlm  22250  tx1stc  22252  txkgen  22254  cnmpt21  22273  txswaphmeolem  22406  txswaphmeo  22407  clssubg  22711  qustgplem  22723  comet  23117  txmetcnp  23151  metustsym  23159  nrmmetd  23178  isngp3  23201  ngpds  23207  qtopbaslem  23361  cnmetdval  23373  remetdval  23391  tgqioo  23402  bndth  23556  htpyco2  23577  phtpyco2  23588  ovolicc1  24111  ioorf  24168  ioorcl  24172  itg1addlem4  24294  dvcnp2  24511  dvef  24571  lhop1lem  24604  taylthlem2  24956  addsqnreup  26013  brcgr  26680  ex-fpar  28235  imsdval  28457  sspval  28494  opreu2reuALT  30234  ofoprabco  30403  f1od2  30451  qtophaus  31095  mbfmco2  31518  eulerpartlemgh  31631  afsval  31937  erdszelem9  32441  cvmlift2lem1  32544  cvmlift2lem9  32553  cvmlift2lem12  32556  cvmlift2lem13  32557  cvmliftphtlem  32559  goel  32589  goelel3xp  32590  sat1el2xp  32621  fmla0xp  32625  prv1n  32673  msubco  32773  msubff1  32798  mvhf  32800  msubvrs  32802  fvtransport  33488  colinearex  33516  bj-idres  34446  icoreunrn  34634  relowlpssretop  34639  curf  34864  finixpnum  34871  poimirlem3  34889  poimirlem4  34890  poimirlem15  34901  poimirlem17  34903  poimirlem20  34906  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  heicant  34921  mblfinlem1  34923  mblfinlem2  34924  ftc1anc  34969  opropabco  34993  heiborlem5  35087  dvhelvbasei  38218  dvhopvadd  38223  dvhvaddcl  38225  dvhopvsca  38232  dvhvscacl  38233  dvhgrp  38237  dvhopclN  38243  dvhopaddN  38244  dvhopspN  38245  dib1dim2  38298  diblss  38300  diclspsn  38324  dih1dimatlem  38459  opelxpii  39110  hoicvr  42824  hoicvrrex  42832  ovnsubaddlem1  42846  ovnhoilem1  42877  ovnlecvr2  42886  opnvonmbllem1  42908  ovolval4lem2  42926  fnotaovb  43391  aovmpt4g  43394  rngccoALTV  44253  ringccoALTV  44316  rhmsubclem2  44352  rhmsubcALTVlem2  44370  rrx2plordisom  44704