Theorem opelxpi 4630

Description: Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opelxpi	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpi

Step	Hyp	Ref	Expression
1		opelxp 4628	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 132	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2135  ⟨cop 3573   × cxp 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2723  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-opab 4038  df-xp 4604

This theorem is referenced by:  opelxpd  4631  opelvvg  4647  opelvv  4648  opbrop  4677  fliftrel  5754  fnotovb  5876  ovi3  5969  ovres  5972  fovrn  5975  fnovrn  5980  ovconst2  5984  oprab2co  6177  1stconst  6180  2ndconst  6181  f1od2  6194  brdifun  6519  ecopqsi  6547  brecop  6582  th3q  6597  xpcomco  6783  xpf1o  6801  xpmapenlem  6806  djulclr  7005  djurclr  7006  djulcl  7007  djurcl  7008  djuf1olem  7009  cc2lem  7198  addpiord  7248  mulpiord  7249  enqeceq  7291  1nq  7298  addpipqqslem  7301  mulpipq  7304  mulpipqqs  7305  addclnq  7307  mulclnq  7308  recexnq  7322  ltexnqq  7340  prarloclemarch  7350  prarloclemarch2  7351  nnnq  7354  enq0breq  7368  enq0eceq  7369  nqnq0  7373  addnnnq0  7381  mulnnnq0  7382  addclnq0  7383  mulclnq0  7384  nqpnq0nq  7385  prarloclemlt  7425  prarloclemlo  7426  prarloclemcalc  7434  genpelxp  7443  nqprm  7474  ltexprlempr  7540  recexprlempr  7564  cauappcvgprlemcl  7585  cauappcvgprlemladd  7590  caucvgprlemcl  7608  caucvgprprlemcl  7636  enreceq  7668  addsrpr  7677  mulsrpr  7678  0r  7682  1sr  7683  m1r  7684  addclsr  7685  mulclsr  7686  prsrcl  7716  mappsrprg  7736  addcnsr  7766  mulcnsr  7767  addcnsrec  7774  mulcnsrec  7775  pitonnlem2  7779  pitonn  7780  pitore  7782  recnnre  7783  axaddcl  7796  axmulcl  7798  xrlenlt  7954  frecuzrdgg  10341  frecuzrdgsuctlem  10348  seq3val  10383  cnrecnv  10838  eucalgf  11966  eucalg  11970  qredeu  12008  qnumdenbi  12101  crth  12133  phimullem  12134  setscom  12371  setsslid  12381  txbas  12799  upxp  12813  uptx  12815  txlm  12820  cnmpt21  12832  txswaphmeolem  12861  txswaphmeo  12862  comet  13040  qtopbasss  13062  cnmetdval  13070  remetdval  13080  tgqioo  13088  dvcnp2cntop  13204  dvef  13229  djucllem  13516  pwle2  13712