Theorem opelxpi 4691

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  ⟨cop 3621   × cxp 4657

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-opab 4091  df-xp 4665

This theorem is referenced by:  opelxpd  4692  opelvvg  4708  opelvv  4709  opbrop  4738  fliftrel  5835  fnotovb  5961  ovi3  6055  ovres  6058  fovcdm  6061  fnovrn  6066  ovconst2  6070  oprab2co  6271  1stconst  6274  2ndconst  6275  f1od2  6288  brdifun  6614  ecopqsi  6644  brecop  6679  th3q  6694  xpcomco  6880  xpf1o  6900  xpmapenlem  6905  djulclr  7108  djurclr  7109  djulcl  7110  djurcl  7111  djuf1olem  7112  cc2lem  7326  addpiord  7376  mulpiord  7377  enqeceq  7419  1nq  7426  addpipqqslem  7429  mulpipq  7432  mulpipqqs  7433  addclnq  7435  mulclnq  7436  recexnq  7450  ltexnqq  7468  prarloclemarch  7478  prarloclemarch2  7479  nnnq  7482  enq0breq  7496  enq0eceq  7497  nqnq0  7501  addnnnq0  7509  mulnnnq0  7510  addclnq0  7511  mulclnq0  7512  nqpnq0nq  7513  prarloclemlt  7553  prarloclemlo  7554  prarloclemcalc  7562  genpelxp  7571  nqprm  7602  ltexprlempr  7668  recexprlempr  7692  cauappcvgprlemcl  7713  cauappcvgprlemladd  7718  caucvgprlemcl  7736  caucvgprprlemcl  7764  enreceq  7796  addsrpr  7805  mulsrpr  7806  0r  7810  1sr  7811  m1r  7812  addclsr  7813  mulclsr  7814  prsrcl  7844  mappsrprg  7864  addcnsr  7894  mulcnsr  7895  addcnsrec  7902  mulcnsrec  7903  pitonnlem2  7907  pitonn  7908  pitore  7910  recnnre  7911  axaddcl  7924  axmulcl  7926  xrlenlt  8084  frecuzrdgg  10487  frecuzrdgsuctlem  10494  seq3val  10531  cnrecnv  11054  eucalgf  12193  eucalg  12197  qredeu  12235  qnumdenbi  12330  crth  12362  phimullem  12363  setscom  12658  setsslid  12669  imasaddfnlemg  12897  imasaddflemg  12899  txbas  14426  upxp  14440  uptx  14442  txlm  14447  cnmpt21  14459  txswaphmeolem  14488  txswaphmeo  14489  comet  14667  qtopbasss  14689  cnmetdval  14697  remetdval  14707  tgqioo  14715  dvcnp2cntop  14848  dvef  14873  djucllem  15292  pwle2  15489