Theorem opelxpi 4751

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ⟨cop 3669   × cxp 4717

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-opab 4146  df-xp 4725

This theorem is referenced by:  opelxpd  4752  opelvvg  4768  opelvv  4769  opbrop  4798  fnbrfvb2  5678  fliftrel  5922  fnotovb  6053  ovi3  6148  ovres  6151  fovcdm  6154  fnovrn  6159  ovconst2  6163  oprab2co  6370  1stconst  6373  2ndconst  6374  f1od2  6387  brdifun  6715  ecopqsi  6745  brecop  6780  th3q  6795  xpcomco  6993  xpf1o  7013  xpmapenlem  7018  djulclr  7227  djurclr  7228  djulcl  7229  djurcl  7230  djuf1olem  7231  cc2lem  7463  addpiord  7514  mulpiord  7515  enqeceq  7557  1nq  7564  addpipqqslem  7567  mulpipq  7570  mulpipqqs  7571  addclnq  7573  mulclnq  7574  recexnq  7588  ltexnqq  7606  prarloclemarch  7616  prarloclemarch2  7617  nnnq  7620  enq0breq  7634  enq0eceq  7635  nqnq0  7639  addnnnq0  7647  mulnnnq0  7648  addclnq0  7649  mulclnq0  7650  nqpnq0nq  7651  prarloclemlt  7691  prarloclemlo  7692  prarloclemcalc  7700  genpelxp  7709  nqprm  7740  ltexprlempr  7806  recexprlempr  7830  cauappcvgprlemcl  7851  cauappcvgprlemladd  7856  caucvgprlemcl  7874  caucvgprprlemcl  7902  enreceq  7934  addsrpr  7943  mulsrpr  7944  0r  7948  1sr  7949  m1r  7950  addclsr  7951  mulclsr  7952  prsrcl  7982  mappsrprg  8002  addcnsr  8032  mulcnsr  8033  addcnsrec  8040  mulcnsrec  8041  pitonnlem2  8045  pitonn  8046  pitore  8048  recnnre  8049  axaddcl  8062  axmulcl  8064  xrlenlt  8222  frecuzrdgg  10650  frecuzrdgsuctlem  10657  seq3val  10694  swrdval  11196  cnrecnv  11437  eucalgf  12593  eucalg  12597  qredeu  12635  qnumdenbi  12730  crth  12762  phimullem  12763  setscom  13088  setsslid  13099  imasaddfnlemg  13363  imasaddflemg  13365  txbas  14948  upxp  14962  uptx  14964  txlm  14969  cnmpt21  14981  txswaphmeolem  15010  txswaphmeo  15011  comet  15189  qtopbasss  15211  cnmetdval  15219  remetdval  15237  tgqioo  15245  dvcnp2cntop  15389  dvef  15417  djucllem  16247  pwle2  16451