Theorem opelxpi 5691

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ⟨cop 4607   × cxp 5652

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-opab 5182  df-xp 5660

This theorem is referenced by:  opelxpii  5692  opelxpd  5693  opelvv  5694  opelvvg  5695  opbrop  5752  elsnxp  6280  reuop  6282  fnbrfvb2  6934  ov3  7570  ovres  7573  fovcdm  7577  fnovrn  7582  ovima0  7586  ovconst2  7587  el2xptp0  8035  opiota  8058  fimaproj  8134  xpord2pred  8144  seqomlem2  8465  brdifun  8749  ecopqsi  8788  brecop  8824  eceqoveq  8836  xpcomco  9076  djulcl  9924  djurcl  9925  djulf1o  9926  djurf1o  9927  djuun  9940  isfin4p1  10329  axdc4lem  10469  canthp1lem2  10667  addpiord  10898  mulpiord  10899  pinq  10941  nqereu  10943  addpipq  10951  addpqnq  10952  mulpipq  10954  mulpqnq  10955  ordpipq  10956  recmulnq  10978  dmrecnq  10982  enreceq  11080  addsrpr  11089  mulsrpr  11090  0r  11094  1sr  11095  m1r  11096  addclsr  11097  mulclsr  11098  axaddf  11159  xrlenlt  11300  uzrdgfni  13976  swrdval  14661  ruclem6  16253  eucalgf  16602  eucalg  16606  qnumdenbi  16763  setscom  17199  strfv2d  17220  setsid  17226  imasaddfnlem  17542  imasaddflem  17544  imasvscafn  17551  imasvscaval  17552  funcpropd  17915  fucco  17978  catcxpccl  18219  curf1cl  18240  curf2cl  18243  curfcl  18244  uncfcurf  18251  diag2  18257  curf2ndf  18259  joindmss  18389  meetdmss  18403  latlem  18447  latjcom  18457  latmcom  18473  efgmf  19694  efglem  19697  vrgpf  19749  vrgpinv  19750  frgpuplem  19753  frgpup2  19757  frgpnabllem1  19854  gsumxp2  19961  rhmsubclem2  20646  pzriprnglem10  21451  mamudi  22341  mamudir  22342  mamuvs1  22343  mamuvs2  22344  matsubgcell  22372  matvscacell  22374  pmatcoe1fsupp  22639  txbas  23505  txcls  23542  upxp  23561  uptx  23563  txtube  23578  txcmplem1  23579  txlm  23586  tx1stc  23588  txkgen  23590  cnmpt21  23609  txswaphmeolem  23742  txswaphmeo  23743  clssubg  24047  qustgplem  24059  comet  24452  txmetcnp  24486  metustsym  24494  nrmmetd  24513  isngp3  24537  ngpds  24543  qtopbaslem  24697  cnmetdval  24709  remetdval  24728  tgqioo  24739  bndth  24908  htpyco2  24929  phtpyco2  24940  ovolicc1  25469  ioorf  25526  ioorcl  25530  itg1addlem4  25652  dvcnp2  25873  dvcnp2OLD  25874  dvef  25936  lhop1lem  25970  taylthlem2  26334  taylthlem2OLD  26335  addsqnreup  27406  addsfo  27942  subsfo  28021  noseqrdgfn  28252  brcgr  28879  ex-fpar  30443  imsdval  30667  sspval  30704  opreu2reuALT  32458  2ndimaxp  32624  ofoprabco  32642  f1od2  32698  qtophaus  33867  mbfmco2  34297  eulerpartlemgh  34410  afsval  34703  erdszelem9  35221  cvmlift2lem1  35324  cvmlift2lem9  35333  cvmlift2lem12  35336  cvmlift2lem13  35337  cvmliftphtlem  35339  goel  35369  goelel3xp  35370  sat1el2xp  35401  fmla0xp  35405  prv1n  35453  msubco  35553  msubff1  35578  mvhf  35580  msubvrs  35582  fvtransport  36050  colinearex  36078  bj-idres  37178  icoreunrn  37377  relowlpssretop  37382  curf  37622  finixpnum  37629  poimirlem15  37659  poimirlem25  37669  poimirlem26  37670  poimirlem27  37671  heicant  37679  mblfinlem1  37681  mblfinlem2  37682  ftc1anc  37725  opropabco  37748  heiborlem5  37839  dvhelvbasei  41107  dvhopvadd  41112  dvhvaddcl  41114  dvhopvsca  41121  dvhvscacl  41122  dvhgrp  41126  dvhopclN  41132  dvhopaddN  41133  dvhopspN  41134  dib1dim2  41187  diblss  41189  diclspsn  41213  dih1dimatlem  41348  hoicvr  46577  hoicvrrex  46585  ovnsubaddlem1  46599  ovnhoilem1  46630  ovnlecvr2  46639  opnvonmbllem1  46661  ovolval4lem2  46679  fnotaovb  47227  aovmpt4g  47230  rngccoALTV  48246  rhmsubcALTVlem2  48257  ringccoALTV  48280  rrx2plordisom  48703