Theorem opelxpi 4763

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ⟨cop 3676   × cxp 4729

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-opab 4156  df-xp 4737

This theorem is referenced by:  opelxpd  4764  opelvvg  4781  opelvv  4782  opbrop  4811  fnbrfvb2  5697  fliftrel  5943  fnotovb  6074  ovi3  6169  ovres  6172  fovcdm  6175  fnovrn  6180  ovconst2  6184  oprab2co  6392  1stconst  6395  2ndconst  6396  f1od2  6409  brdifun  6772  ecopqsi  6802  brecop  6837  th3q  6852  xpcomco  7053  xpf1o  7073  xpmapenlem  7078  djulclr  7308  djurclr  7309  djulcl  7310  djurcl  7311  djuf1olem  7312  cc2lem  7545  addpiord  7596  mulpiord  7597  enqeceq  7639  1nq  7646  addpipqqslem  7649  mulpipq  7652  mulpipqqs  7653  addclnq  7655  mulclnq  7656  recexnq  7670  ltexnqq  7688  prarloclemarch  7698  prarloclemarch2  7699  nnnq  7702  enq0breq  7716  enq0eceq  7717  nqnq0  7721  addnnnq0  7729  mulnnnq0  7730  addclnq0  7731  mulclnq0  7732  nqpnq0nq  7733  prarloclemlt  7773  prarloclemlo  7774  prarloclemcalc  7782  genpelxp  7791  nqprm  7822  ltexprlempr  7888  recexprlempr  7912  cauappcvgprlemcl  7933  cauappcvgprlemladd  7938  caucvgprlemcl  7956  caucvgprprlemcl  7984  enreceq  8016  addsrpr  8025  mulsrpr  8026  0r  8030  1sr  8031  m1r  8032  addclsr  8033  mulclsr  8034  prsrcl  8064  mappsrprg  8084  addcnsr  8114  mulcnsr  8115  addcnsrec  8122  mulcnsrec  8123  pitonnlem2  8127  pitonn  8128  pitore  8130  recnnre  8131  axaddcl  8144  axmulcl  8146  xrlenlt  8303  frecuzrdgg  10741  frecuzrdgsuctlem  10748  seq3val  10785  swrdval  11295  cnrecnv  11550  eucalgf  12707  eucalg  12711  qredeu  12749  qnumdenbi  12844  crth  12876  phimullem  12877  setscom  13202  setsslid  13213  imasaddfnlemg  13477  imasaddflemg  13479  txbas  15069  upxp  15083  uptx  15085  txlm  15090  cnmpt21  15102  txswaphmeolem  15131  txswaphmeo  15132  comet  15310  qtopbasss  15332  cnmetdval  15340  remetdval  15358  tgqioo  15366  dvcnp2cntop  15510  dvef  15538  djucllem  16518  pwle2  16720