Theorem opelxpi 4786

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ⟨cop 3697   × cxp 4752

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 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-opab 4177  df-xp 4760

This theorem is referenced by:  opelxpd  4787  opelvvg  4804  opelvv  4805  opbrop  4834  fnbrfvb2  5724  fliftrel  5971  fnotovb  6104  ovi3  6199  ovres  6202  fovcdm  6205  fnovrn  6210  ovconst2  6214  oprab2co  6427  1stconst  6430  2ndconst  6431  f1od2  6444  brdifun  6807  ecopqsi  6837  brecop  6872  th3q  6887  xpcomco  7090  xpf1o  7110  xpmapenlem  7115  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djuf1olem  7357  cc2lem  7596  addpiord  7647  mulpiord  7648  enqeceq  7690  1nq  7697  addpipqqslem  7700  mulpipq  7703  mulpipqqs  7704  addclnq  7706  mulclnq  7707  recexnq  7721  ltexnqq  7739  prarloclemarch  7749  prarloclemarch2  7750  nnnq  7753  enq0breq  7767  enq0eceq  7768  nqnq0  7772  addnnnq0  7780  mulnnnq0  7781  addclnq0  7782  mulclnq0  7783  nqpnq0nq  7784  prarloclemlt  7824  prarloclemlo  7825  prarloclemcalc  7833  genpelxp  7842  nqprm  7873  ltexprlempr  7939  recexprlempr  7963  cauappcvgprlemcl  7984  cauappcvgprlemladd  7989  caucvgprlemcl  8007  caucvgprprlemcl  8035  enreceq  8067  addsrpr  8076  mulsrpr  8077  0r  8081  1sr  8082  m1r  8083  addclsr  8084  mulclsr  8085  prsrcl  8115  mappsrprg  8135  addcnsr  8165  mulcnsr  8166  addcnsrec  8173  mulcnsrec  8174  pitonnlem2  8178  pitonn  8179  pitore  8181  recnnre  8182  axaddcl  8195  axmulcl  8197  xrlenlt  8354  frecuzrdgg  10802  frecuzrdgsuctlem  10809  seq3val  10846  swrdval  11365  cnrecnv  11620  eucalgf  12777  eucalg  12781  qredeu  12819  qnumdenbi  12914  crth  12946  phimullem  12947  setscom  13336  setsslid  13347  imasaddfnlemg  13578  imasaddflemg  13580  txbas  15249  upxp  15263  uptx  15265  txlm  15270  cnmpt21  15282  txswaphmeolem  15311  txswaphmeo  15312  comet  15490  qtopbasss  15512  cnmetdval  15520  remetdval  15538  tgqioo  15546  dvcnp2cntop  15690  dvef  15718  djucllem  16698  pwle2  16898