Theorem opelxpi 4442

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

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1436  ⟨cop 3434   × cxp 4409

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3932  ax-pow 3984  ax-pr 4010

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-opab 3875  df-xp 4417

This theorem is referenced by:  opelvvg  4455  opelvv  4456  opbrop  4485  fliftrel  5532  fnotovb  5649  ovi3  5738  ovres  5741  fovrn  5744  fnovrn  5749  ovconst2  5753  oprab2co  5940  1stconst  5943  2ndconst  5944  f1od2  5957  brdifun  6271  ecopqsi  6299  brecop  6334  th3q  6349  xpcomco  6494  xpf1o  6512  xpmapenlem  6517  djulclr  6685  djurclr  6686  djulcl  6687  djurcl  6688  djuf1olem  6689  addpiord  6819  mulpiord  6820  enqeceq  6862  1nq  6869  addpipqqslem  6872  mulpipq  6875  mulpipqqs  6876  addclnq  6878  mulclnq  6879  recexnq  6893  ltexnqq  6911  prarloclemarch  6921  prarloclemarch2  6922  nnnq  6925  enq0breq  6939  enq0eceq  6940  nqnq0  6944  addnnnq0  6952  mulnnnq0  6953  addclnq0  6954  mulclnq0  6955  nqpnq0nq  6956  prarloclemlt  6996  prarloclemlo  6997  prarloclemcalc  7005  genpelxp  7014  nqprm  7045  ltexprlempr  7111  recexprlempr  7135  cauappcvgprlemcl  7156  cauappcvgprlemladd  7161  caucvgprlemcl  7179  caucvgprprlemcl  7207  enreceq  7226  addsrpr  7235  mulsrpr  7236  0r  7240  1sr  7241  m1r  7242  addclsr  7243  mulclsr  7244  prsrcl  7273  addcnsr  7315  mulcnsr  7316  addcnsrec  7323  mulcnsrec  7324  pitonnlem2  7328  pitonn  7329  pitore  7331  recnnre  7332  axaddcl  7345  axmulcl  7347  xrlenlt  7495  frecuzrdgg  9751  frecuzrdgsuctlem  9758  iseqvalt  9790  cnrecnv  10239  eucalgf  10912  eucialg  10916  qredeu  10954  qnumdenbi  11045  crth  11075  phimullem  11076  djucllem  11138