Theorem opelxpi 4781

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  ⟨cop 3692   × cxp 4747

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-opab 4172  df-xp 4755

This theorem is referenced by:  opelxpd  4782  opelvvg  4799  opelvv  4800  opbrop  4829  fnbrfvb2  5719  fliftrel  5965  fnotovb  6096  ovi3  6191  ovres  6194  fovcdm  6197  fnovrn  6202  ovconst2  6206  oprab2co  6414  1stconst  6417  2ndconst  6418  f1od2  6431  brdifun  6794  ecopqsi  6824  brecop  6859  th3q  6874  xpcomco  7077  xpf1o  7097  xpmapenlem  7102  djulclr  7340  djurclr  7341  djulcl  7342  djurcl  7343  djuf1olem  7344  cc2lem  7580  addpiord  7631  mulpiord  7632  enqeceq  7674  1nq  7681  addpipqqslem  7684  mulpipq  7687  mulpipqqs  7688  addclnq  7690  mulclnq  7691  recexnq  7705  ltexnqq  7723  prarloclemarch  7733  prarloclemarch2  7734  nnnq  7737  enq0breq  7751  enq0eceq  7752  nqnq0  7756  addnnnq0  7764  mulnnnq0  7765  addclnq0  7766  mulclnq0  7767  nqpnq0nq  7768  prarloclemlt  7808  prarloclemlo  7809  prarloclemcalc  7817  genpelxp  7826  nqprm  7857  ltexprlempr  7923  recexprlempr  7947  cauappcvgprlemcl  7968  cauappcvgprlemladd  7973  caucvgprlemcl  7991  caucvgprprlemcl  8019  enreceq  8051  addsrpr  8060  mulsrpr  8061  0r  8065  1sr  8066  m1r  8067  addclsr  8068  mulclsr  8069  prsrcl  8099  mappsrprg  8119  addcnsr  8149  mulcnsr  8150  addcnsrec  8157  mulcnsrec  8158  pitonnlem2  8162  pitonn  8163  pitore  8165  recnnre  8166  axaddcl  8179  axmulcl  8181  xrlenlt  8338  frecuzrdgg  10778  frecuzrdgsuctlem  10785  seq3val  10822  swrdval  11340  cnrecnv  11595  eucalgf  12752  eucalg  12756  qredeu  12794  qnumdenbi  12889  crth  12921  phimullem  12922  setscom  13252  setsslid  13263  imasaddfnlemg  13527  imasaddflemg  13529  txbas  15123  upxp  15137  uptx  15139  txlm  15144  cnmpt21  15156  txswaphmeolem  15185  txswaphmeo  15186  comet  15364  qtopbasss  15386  cnmetdval  15394  remetdval  15412  tgqioo  15420  dvcnp2cntop  15564  dvef  15592  djucllem  16572  pwle2  16772