Theorem opelxpi 4725

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2178  ⟨cop 3646   × cxp 4691

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-opab 4122  df-xp 4699

This theorem is referenced by:  opelxpd  4726  opelvvg  4742  opelvv  4743  opbrop  4772  fliftrel  5884  fnotovb  6011  ovi3  6106  ovres  6109  fovcdm  6112  fnovrn  6117  ovconst2  6121  oprab2co  6327  1stconst  6330  2ndconst  6331  f1od2  6344  brdifun  6670  ecopqsi  6700  brecop  6735  th3q  6750  xpcomco  6946  xpf1o  6966  xpmapenlem  6971  djulclr  7177  djurclr  7178  djulcl  7179  djurcl  7180  djuf1olem  7181  cc2lem  7413  addpiord  7464  mulpiord  7465  enqeceq  7507  1nq  7514  addpipqqslem  7517  mulpipq  7520  mulpipqqs  7521  addclnq  7523  mulclnq  7524  recexnq  7538  ltexnqq  7556  prarloclemarch  7566  prarloclemarch2  7567  nnnq  7570  enq0breq  7584  enq0eceq  7585  nqnq0  7589  addnnnq0  7597  mulnnnq0  7598  addclnq0  7599  mulclnq0  7600  nqpnq0nq  7601  prarloclemlt  7641  prarloclemlo  7642  prarloclemcalc  7650  genpelxp  7659  nqprm  7690  ltexprlempr  7756  recexprlempr  7780  cauappcvgprlemcl  7801  cauappcvgprlemladd  7806  caucvgprlemcl  7824  caucvgprprlemcl  7852  enreceq  7884  addsrpr  7893  mulsrpr  7894  0r  7898  1sr  7899  m1r  7900  addclsr  7901  mulclsr  7902  prsrcl  7932  mappsrprg  7952  addcnsr  7982  mulcnsr  7983  addcnsrec  7990  mulcnsrec  7991  pitonnlem2  7995  pitonn  7996  pitore  7998  recnnre  7999  axaddcl  8012  axmulcl  8014  xrlenlt  8172  frecuzrdgg  10598  frecuzrdgsuctlem  10605  seq3val  10642  swrdval  11139  cnrecnv  11336  eucalgf  12492  eucalg  12496  qredeu  12534  qnumdenbi  12629  crth  12661  phimullem  12662  setscom  12987  setsslid  12998  imasaddfnlemg  13261  imasaddflemg  13263  txbas  14845  upxp  14859  uptx  14861  txlm  14866  cnmpt21  14878  txswaphmeolem  14907  txswaphmeo  14908  comet  15086  qtopbasss  15108  cnmetdval  15116  remetdval  15134  tgqioo  15142  dvcnp2cntop  15286  dvef  15314  djucllem  15936  pwle2  16137