Theorem opelxpi 4755

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ⟨cop 3670   × cxp 4721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-opab 4149  df-xp 4729

This theorem is referenced by:  opelxpd  4756  opelvvg  4773  opelvv  4774  opbrop  4803  fnbrfvb2  5684  fliftrel  5928  fnotovb  6059  ovi3  6154  ovres  6157  fovcdm  6160  fnovrn  6165  ovconst2  6169  oprab2co  6378  1stconst  6381  2ndconst  6382  f1od2  6395  brdifun  6724  ecopqsi  6754  brecop  6789  th3q  6804  xpcomco  7005  xpf1o  7025  xpmapenlem  7030  djulclr  7239  djurclr  7240  djulcl  7241  djurcl  7242  djuf1olem  7243  cc2lem  7475  addpiord  7526  mulpiord  7527  enqeceq  7569  1nq  7576  addpipqqslem  7579  mulpipq  7582  mulpipqqs  7583  addclnq  7585  mulclnq  7586  recexnq  7600  ltexnqq  7618  prarloclemarch  7628  prarloclemarch2  7629  nnnq  7632  enq0breq  7646  enq0eceq  7647  nqnq0  7651  addnnnq0  7659  mulnnnq0  7660  addclnq0  7661  mulclnq0  7662  nqpnq0nq  7663  prarloclemlt  7703  prarloclemlo  7704  prarloclemcalc  7712  genpelxp  7721  nqprm  7752  ltexprlempr  7818  recexprlempr  7842  cauappcvgprlemcl  7863  cauappcvgprlemladd  7868  caucvgprlemcl  7886  caucvgprprlemcl  7914  enreceq  7946  addsrpr  7955  mulsrpr  7956  0r  7960  1sr  7961  m1r  7962  addclsr  7963  mulclsr  7964  prsrcl  7994  mappsrprg  8014  addcnsr  8044  mulcnsr  8045  addcnsrec  8052  mulcnsrec  8053  pitonnlem2  8057  pitonn  8058  pitore  8060  recnnre  8061  axaddcl  8074  axmulcl  8076  xrlenlt  8234  frecuzrdgg  10668  frecuzrdgsuctlem  10675  seq3val  10712  swrdval  11219  cnrecnv  11461  eucalgf  12617  eucalg  12621  qredeu  12659  qnumdenbi  12754  crth  12786  phimullem  12787  setscom  13112  setsslid  13123  imasaddfnlemg  13387  imasaddflemg  13389  txbas  14972  upxp  14986  uptx  14988  txlm  14993  cnmpt21  15005  txswaphmeolem  15034  txswaphmeo  15035  comet  15213  qtopbasss  15235  cnmetdval  15243  remetdval  15261  tgqioo  15269  dvcnp2cntop  15413  dvef  15441  djucllem  16332  pwle2  16535