Theorem opelxpi 5698

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2143  ⟨cop 4595   × cxp 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5174  df-xp 5667

This theorem is used by:  opelxpii  5699  opelxpd  5700  opelvv  5701  opelvvg  5702  opbrop  5759  elsnxp  6292  reuop  6294  fnbrfvb2  6936  ov3  7573  ovres  7576  fovcdm  7580  fnovrn  7585  ovima0  7589  ovconst2  7590  el2xptp0  8029  opiota  8052  fimaproj  8127  xpord2pred  8137  seqomlem2  8434  brdifun  8721  ecopqsi  8764  brecop  8804  eceqoveq  8816  xpcomco  9051  djulcl  9901  djurcl  9902  djulf1o  9903  djurf1o  9904  djuun  9917  isfin4p1  10303  axdc4lem  10443  canthp1lem2  10642  addpiord  10873  mulpiord  10874  pinq  10916  nqereu  10918  addpipq  10926  addpqnq  10927  mulpipq  10929  mulpqnq  10930  ordpipq  10931  recmulnq  10953  dmrecnq  10957  enreceq  11055  addsrpr  11064  mulsrpr  11065  0r  11069  1sr  11070  m1r  11071  addclsr  11072  mulclsr  11073  axaddf  11134  xrlenlt  11278  uzrdgfni  13999  swrdval  14686  ruclem6  16295  eucalgf  16645  eucalg  16649  qnumdenbi  16807  setscom  17244  strfv2d  17265  setsid  17271  imasaddfnlem  17586  imasaddflem  17588  imasvscafn  17595  imasvscaval  17596  funcpropd  17963  fucco  18026  catcxpccl  18267  curf1cl  18288  curf2cl  18291  curfcl  18292  uncfcurf  18299  diag2  18305  curf2ndf  18307  joindmss  18437  meetdmss  18451  latlem  18497  latjcom  18507  latmcom  18523  efgmf  19787  efglem  19790  vrgpf  19842  vrgpinv  19843  frgpuplem  19846  frgpup2  19850  frgpnabllem1  19947  gsumxp2  20054  rhmsubclem2  20794  pzriprnglem10  21649  mamudi  22569  mamudir  22570  mamuvs1  22571  mamuvs2  22572  matsubgcell  22600  matvscacell  22602  pmatcoe1fsupp  22867  txbas  23733  txcls  23770  upxp  23789  uptx  23791  txtube  23806  txcmplem1  23807  txlm  23814  tx1stc  23816  txkgen  23818  cnmpt21  23837  txswaphmeolem  23970  txswaphmeo  23971  clssubg  24275  qustgplem  24287  comet  24679  txmetcnp  24713  metustsym  24721  nrmmetd  24740  isngp3  24764  ngpds  24770  qtopbaslem  24924  cnmetdval  24936  remetdval  24955  tgqioo  24966  bndth  25126  htpyco2  25147  phtpyco2  25158  ovolicc1  25684  ioorf  25741  ioorcl  25745  itg1addlem4  25867  dvcnp2  26088  dvef  26148  lhop1lem  26181  taylthlem2  26546  addsqnreup  27616  addsfo  28185  subsfo  28267  noseqrdgfn  28508  brcgr  29259  ex-fpar  30822  imsdval  31047  sspval  31084  opreu2reuALT  32832  2ndimaxp  33000  ofoprabco  33018  f1od2  33073  qtophaus  34235  mbfmco2  34664  eulerpartlemgh  34777  afsval  35070  erdszelem9  35699  cvmlift2lem1  35802  cvmlift2lem9  35811  cvmlift2lem12  35814  cvmlift2lem13  35815  cvmliftphtlem  35817  goel  35847  goelel3xp  35848  sat1el2xp  35879  fmla0xp  35883  prv1n  35931  msubco  36031  msubff1  36056  mvhf  36058  msubvrs  36060  fvtransport  36532  colinearex  36560  nmulprop  36690  bj-idres  37832  icoreunrn  38033  relowlpssretop  38038  curf  38277  finixpnum  38284  poimirlem15  38314  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  heicant  38334  mblfinlem1  38336  mblfinlem2  38337  ftc1anc  38380  opropabco  38403  heiborlem5  38494  dvhelvbasei  41890  dvhopvadd  41895  dvhvaddcl  41897  dvhopvsca  41904  dvhvscacl  41905  dvhgrp  41909  dvhopclN  41915  dvhopaddN  41916  dvhopspN  41917  dib1dim2  41970  diblss  41972  diclspsn  41996  dih1dimatlem  42131  hoicvrrex  47298  ovnsubaddlem1  47312  ovnhoilem1  47343  ovnlecvr2  47352  opnvonmbllem1  47374  ovolval4lem2  47392  fnotaovb  47963  aovmpt4g  47966  rngccoALTV  49064  rhmsubcALTVlem2  49075  ringccoALTV  49098  rrx2plordisom  49531