Theorem opelxpi 4757

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

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

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-opab 4151  df-xp 4731

This theorem is referenced by:  opelxpd  4758  opelvvg  4775  opelvv  4776  opbrop  4805  fnbrfvb2  5688  fliftrel  5933  fnotovb  6064  ovi3  6159  ovres  6162  fovcdm  6165  fnovrn  6170  ovconst2  6174  oprab2co  6383  1stconst  6386  2ndconst  6387  f1od2  6400  brdifun  6729  ecopqsi  6759  brecop  6794  th3q  6809  xpcomco  7010  xpf1o  7030  xpmapenlem  7035  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djuf1olem  7252  cc2lem  7485  addpiord  7536  mulpiord  7537  enqeceq  7579  1nq  7586  addpipqqslem  7589  mulpipq  7592  mulpipqqs  7593  addclnq  7595  mulclnq  7596  recexnq  7610  ltexnqq  7628  prarloclemarch  7638  prarloclemarch2  7639  nnnq  7642  enq0breq  7656  enq0eceq  7657  nqnq0  7661  addnnnq0  7669  mulnnnq0  7670  addclnq0  7671  mulclnq0  7672  nqpnq0nq  7673  prarloclemlt  7713  prarloclemlo  7714  prarloclemcalc  7722  genpelxp  7731  nqprm  7762  ltexprlempr  7828  recexprlempr  7852  cauappcvgprlemcl  7873  cauappcvgprlemladd  7878  caucvgprlemcl  7896  caucvgprprlemcl  7924  enreceq  7956  addsrpr  7965  mulsrpr  7966  0r  7970  1sr  7971  m1r  7972  addclsr  7973  mulclsr  7974  prsrcl  8004  mappsrprg  8024  addcnsr  8054  mulcnsr  8055  addcnsrec  8062  mulcnsrec  8063  pitonnlem2  8067  pitonn  8068  pitore  8070  recnnre  8071  axaddcl  8084  axmulcl  8086  xrlenlt  8244  frecuzrdgg  10679  frecuzrdgsuctlem  10686  seq3val  10723  swrdval  11233  cnrecnv  11488  eucalgf  12645  eucalg  12649  qredeu  12687  qnumdenbi  12782  crth  12814  phimullem  12815  setscom  13140  setsslid  13151  imasaddfnlemg  13415  imasaddflemg  13417  txbas  15001  upxp  15015  uptx  15017  txlm  15022  cnmpt21  15034  txswaphmeolem  15063  txswaphmeo  15064  comet  15242  qtopbasss  15264  cnmetdval  15272  remetdval  15290  tgqioo  15298  dvcnp2cntop  15442  dvef  15470  djucllem  16447  pwle2  16650