Theorem opelxpi 4432

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

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1434  ⟨cop 3425   × cxp 4399

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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 4000

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-opab 3866  df-xp 4407

This theorem is referenced by:  opelvvg  4445  opelvv  4446  opbrop  4475  fliftrel  5511  fnotovb  5627  ovi3  5716  ovres  5719  fovrn  5722  fnovrn  5727  ovconst2  5731  oprab2co  5918  1stconst  5921  2ndconst  5922  f1od2  5935  brdifun  6249  ecopqsi  6277  brecop  6312  th3q  6327  xpcomco  6472  xpf1o  6490  xpmapenlem  6495  djulclr  6648  djurclr  6649  djulcl  6650  djurcl  6651  djuf1olem  6652  addpiord  6778  mulpiord  6779  enqeceq  6821  1nq  6828  addpipqqslem  6831  mulpipq  6834  mulpipqqs  6835  addclnq  6837  mulclnq  6838  recexnq  6852  ltexnqq  6870  prarloclemarch  6880  prarloclemarch2  6881  nnnq  6884  enq0breq  6898  enq0eceq  6899  nqnq0  6903  addnnnq0  6911  mulnnnq0  6912  addclnq0  6913  mulclnq0  6914  nqpnq0nq  6915  prarloclemlt  6955  prarloclemlo  6956  prarloclemcalc  6964  genpelxp  6973  nqprm  7004  ltexprlempr  7070  recexprlempr  7094  cauappcvgprlemcl  7115  cauappcvgprlemladd  7120  caucvgprlemcl  7138  caucvgprprlemcl  7166  enreceq  7185  addsrpr  7194  mulsrpr  7195  0r  7199  1sr  7200  m1r  7201  addclsr  7202  mulclsr  7203  prsrcl  7232  addcnsr  7274  mulcnsr  7275  addcnsrec  7282  mulcnsrec  7283  pitonnlem2  7287  pitonn  7288  pitore  7290  recnnre  7291  axaddcl  7304  axmulcl  7306  xrlenlt  7454  frecuzrdgg  9712  frecuzrdgsuctlem  9719  iseqvalt  9751  cnrecnv  10171  eucalgf  10817  eucialg  10821  qredeu  10859  qnumdenbi  10950  crth  10980  phimullem  10981  djucllem  11043