Theorem opelxpi 4696

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ⟨cop 3626   × cxp 4662

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-opab 4096  df-xp 4670

This theorem is referenced by:  opelxpd  4697  opelvvg  4713  opelvv  4714  opbrop  4743  fliftrel  5842  fnotovb  5969  ovi3  6064  ovres  6067  fovcdm  6070  fnovrn  6075  ovconst2  6079  oprab2co  6285  1stconst  6288  2ndconst  6289  f1od2  6302  brdifun  6628  ecopqsi  6658  brecop  6693  th3q  6708  xpcomco  6894  xpf1o  6914  xpmapenlem  6919  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djuf1olem  7128  cc2lem  7351  addpiord  7402  mulpiord  7403  enqeceq  7445  1nq  7452  addpipqqslem  7455  mulpipq  7458  mulpipqqs  7459  addclnq  7461  mulclnq  7462  recexnq  7476  ltexnqq  7494  prarloclemarch  7504  prarloclemarch2  7505  nnnq  7508  enq0breq  7522  enq0eceq  7523  nqnq0  7527  addnnnq0  7535  mulnnnq0  7536  addclnq0  7537  mulclnq0  7538  nqpnq0nq  7539  prarloclemlt  7579  prarloclemlo  7580  prarloclemcalc  7588  genpelxp  7597  nqprm  7628  ltexprlempr  7694  recexprlempr  7718  cauappcvgprlemcl  7739  cauappcvgprlemladd  7744  caucvgprlemcl  7762  caucvgprprlemcl  7790  enreceq  7822  addsrpr  7831  mulsrpr  7832  0r  7836  1sr  7837  m1r  7838  addclsr  7839  mulclsr  7840  prsrcl  7870  mappsrprg  7890  addcnsr  7920  mulcnsr  7921  addcnsrec  7928  mulcnsrec  7929  pitonnlem2  7933  pitonn  7934  pitore  7936  recnnre  7937  axaddcl  7950  axmulcl  7952  xrlenlt  8110  frecuzrdgg  10527  frecuzrdgsuctlem  10534  seq3val  10571  cnrecnv  11094  eucalgf  12250  eucalg  12254  qredeu  12292  qnumdenbi  12387  crth  12419  phimullem  12420  setscom  12745  setsslid  12756  imasaddfnlemg  13018  imasaddflemg  13020  txbas  14602  upxp  14616  uptx  14618  txlm  14623  cnmpt21  14635  txswaphmeolem  14664  txswaphmeo  14665  comet  14843  qtopbasss  14865  cnmetdval  14873  remetdval  14891  tgqioo  14899  dvcnp2cntop  15043  dvef  15071  djucllem  15554  pwle2  15753