Theorem opelxpi 5722

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

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

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-xp 5691

This theorem is referenced by:  opelxpii  5723  opelxpd  5724  opelvv  5725  opelvvg  5726  opbrop  5783  elsnxp  6311  reuop  6313  fnbrfvb2  6964  ov3  7596  ovres  7599  fovcdm  7603  fnovrn  7608  ovima0  7612  ovconst2  7613  el2xptp0  8061  opiota  8084  fimaproj  8160  xpord2pred  8170  seqomlem2  8491  brdifun  8775  ecopqsi  8814  brecop  8850  eceqoveq  8862  xpcomco  9102  djulcl  9950  djurcl  9951  djulf1o  9952  djurf1o  9953  djuun  9966  isfin4p1  10355  axdc4lem  10495  canthp1lem2  10693  addpiord  10924  mulpiord  10925  pinq  10967  nqereu  10969  addpipq  10977  addpqnq  10978  mulpipq  10980  mulpqnq  10981  ordpipq  10982  recmulnq  11004  dmrecnq  11008  enreceq  11106  addsrpr  11115  mulsrpr  11116  0r  11120  1sr  11121  m1r  11122  addclsr  11123  mulclsr  11124  axaddf  11185  xrlenlt  11326  uzrdgfni  13999  swrdval  14681  ruclem6  16271  eucalgf  16620  eucalg  16624  qnumdenbi  16781  setscom  17217  strfv2d  17238  setsid  17244  imasaddfnlem  17573  imasaddflem  17575  imasvscafn  17582  imasvscaval  17583  funcpropd  17947  fucco  18010  catcxpccl  18252  curf1cl  18273  curf2cl  18276  curfcl  18277  uncfcurf  18284  diag2  18290  curf2ndf  18292  joindmss  18424  meetdmss  18438  latlem  18482  latjcom  18492  latmcom  18508  efgmf  19731  efglem  19734  vrgpf  19786  vrgpinv  19787  frgpuplem  19790  frgpup2  19794  frgpnabllem1  19891  gsumxp2  19998  rhmsubclem2  20686  pzriprnglem10  21501  mamudi  22407  mamudir  22408  mamuvs1  22409  mamuvs2  22410  matsubgcell  22440  matvscacell  22442  pmatcoe1fsupp  22707  txbas  23575  txcls  23612  upxp  23631  uptx  23633  txtube  23648  txcmplem1  23649  txlm  23656  tx1stc  23658  txkgen  23660  cnmpt21  23679  txswaphmeolem  23812  txswaphmeo  23813  clssubg  24117  qustgplem  24129  comet  24526  txmetcnp  24560  metustsym  24568  nrmmetd  24587  isngp3  24611  ngpds  24617  qtopbaslem  24779  cnmetdval  24791  remetdval  24810  tgqioo  24821  bndth  24990  htpyco2  25011  phtpyco2  25022  ovolicc1  25551  ioorf  25608  ioorcl  25612  itg1addlem4  25734  dvcnp2  25955  dvcnp2OLD  25956  dvef  26018  lhop1lem  26052  taylthlem2  26416  taylthlem2OLD  26417  addsqnreup  27487  addsfo  28016  subsfo  28095  noseqrdgfn  28312  brcgr  28915  ex-fpar  30481  imsdval  30705  sspval  30742  opreu2reuALT  32496  2ndimaxp  32656  ofoprabco  32674  f1od2  32732  qtophaus  33835  mbfmco2  34267  eulerpartlemgh  34380  afsval  34686  erdszelem9  35204  cvmlift2lem1  35307  cvmlift2lem9  35316  cvmlift2lem12  35319  cvmlift2lem13  35320  cvmliftphtlem  35322  goel  35352  goelel3xp  35353  sat1el2xp  35384  fmla0xp  35388  prv1n  35436  msubco  35536  msubff1  35561  mvhf  35563  msubvrs  35565  fvtransport  36033  colinearex  36061  bj-idres  37161  icoreunrn  37360  relowlpssretop  37365  curf  37605  finixpnum  37612  poimirlem15  37642  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  heicant  37662  mblfinlem1  37664  mblfinlem2  37665  ftc1anc  37708  opropabco  37731  heiborlem5  37822  dvhelvbasei  41090  dvhopvadd  41095  dvhvaddcl  41097  dvhopvsca  41104  dvhvscacl  41105  dvhgrp  41109  dvhopclN  41115  dvhopaddN  41116  dvhopspN  41117  dib1dim2  41170  diblss  41172  diclspsn  41196  dih1dimatlem  41331  hoicvr  46563  hoicvrrex  46571  ovnsubaddlem1  46585  ovnhoilem1  46616  ovnlecvr2  46625  opnvonmbllem1  46647  ovolval4lem2  46665  fnotaovb  47210  aovmpt4g  47213  rngccoALTV  48187  rhmsubcALTVlem2  48198  ringccoALTV  48221  rrx2plordisom  48644