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  5676  fliftrel  5916  fnotovb  6047  ovi3  6142  ovres  6145  fovcdm  6148  fnovrn  6153  ovconst2  6157  oprab2co  6364  1stconst  6367  2ndconst  6368  f1od2  6381  brdifun  6707  ecopqsi  6737  brecop  6772  th3q  6787  xpcomco  6985  xpf1o  7005  xpmapenlem  7010  djulclr  7216  djurclr  7217  djulcl  7218  djurcl  7219  djuf1olem  7220  cc2lem  7452  addpiord  7503  mulpiord  7504  enqeceq  7546  1nq  7553  addpipqqslem  7556  mulpipq  7559  mulpipqqs  7560  addclnq  7562  mulclnq  7563  recexnq  7577  ltexnqq  7595  prarloclemarch  7605  prarloclemarch2  7606  nnnq  7609  enq0breq  7623  enq0eceq  7624  nqnq0  7628  addnnnq0  7636  mulnnnq0  7637  addclnq0  7638  mulclnq0  7639  nqpnq0nq  7640  prarloclemlt  7680  prarloclemlo  7681  prarloclemcalc  7689  genpelxp  7698  nqprm  7729  ltexprlempr  7795  recexprlempr  7819  cauappcvgprlemcl  7840  cauappcvgprlemladd  7845  caucvgprlemcl  7863  caucvgprprlemcl  7891  enreceq  7923  addsrpr  7932  mulsrpr  7933  0r  7937  1sr  7938  m1r  7939  addclsr  7940  mulclsr  7941  prsrcl  7971  mappsrprg  7991  addcnsr  8021  mulcnsr  8022  addcnsrec  8029  mulcnsrec  8030  pitonnlem2  8034  pitonn  8035  pitore  8037  recnnre  8038  axaddcl  8051  axmulcl  8053  xrlenlt  8211  frecuzrdgg  10638  frecuzrdgsuctlem  10645  seq3val  10682  swrdval  11180  cnrecnv  11421  eucalgf  12577  eucalg  12581  qredeu  12619  qnumdenbi  12714  crth  12746  phimullem  12747  setscom  13072  setsslid  13083  imasaddfnlemg  13347  imasaddflemg  13349  txbas  14932  upxp  14946  uptx  14948  txlm  14953  cnmpt21  14965  txswaphmeolem  14994  txswaphmeo  14995  comet  15173  qtopbasss  15195  cnmetdval  15203  remetdval  15221  tgqioo  15229  dvcnp2cntop  15373  dvef  15401  djucllem  16164  pwle2  16364