ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opelxpi GIF version

Theorem opelxpi 4578
Description: Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)
Assertion
Ref Expression
opelxpi ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpi
StepHypRef Expression
1 opelxp 4576 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21biimpri 132 1 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1481  cop 3534   × cxp 4544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-pr 4138
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-opab 3997  df-xp 4552
This theorem is referenced by:  opelxpd  4579  opelvvg  4595  opelvv  4596  opbrop  4625  fliftrel  5700  fnotovb  5821  ovi3  5914  ovres  5917  fovrn  5920  fnovrn  5925  ovconst2  5929  oprab2co  6122  1stconst  6125  2ndconst  6126  f1od2  6139  brdifun  6463  ecopqsi  6491  brecop  6526  th3q  6541  xpcomco  6727  xpf1o  6745  xpmapenlem  6750  djulclr  6941  djurclr  6942  djulcl  6943  djurcl  6944  djuf1olem  6945  cc2lem  7097  addpiord  7147  mulpiord  7148  enqeceq  7190  1nq  7197  addpipqqslem  7200  mulpipq  7203  mulpipqqs  7204  addclnq  7206  mulclnq  7207  recexnq  7221  ltexnqq  7239  prarloclemarch  7249  prarloclemarch2  7250  nnnq  7253  enq0breq  7267  enq0eceq  7268  nqnq0  7272  addnnnq0  7280  mulnnnq0  7281  addclnq0  7282  mulclnq0  7283  nqpnq0nq  7284  prarloclemlt  7324  prarloclemlo  7325  prarloclemcalc  7333  genpelxp  7342  nqprm  7373  ltexprlempr  7439  recexprlempr  7463  cauappcvgprlemcl  7484  cauappcvgprlemladd  7489  caucvgprlemcl  7507  caucvgprprlemcl  7535  enreceq  7567  addsrpr  7576  mulsrpr  7577  0r  7581  1sr  7582  m1r  7583  addclsr  7584  mulclsr  7585  prsrcl  7615  mappsrprg  7635  addcnsr  7665  mulcnsr  7666  addcnsrec  7673  mulcnsrec  7674  pitonnlem2  7678  pitonn  7679  pitore  7681  recnnre  7682  axaddcl  7695  axmulcl  7697  xrlenlt  7852  frecuzrdgg  10219  frecuzrdgsuctlem  10226  seq3val  10261  cnrecnv  10713  eucalgf  11770  eucalg  11774  qredeu  11812  qnumdenbi  11904  crth  11934  phimullem  11935  setscom  12036  setsslid  12046  txbas  12464  upxp  12478  uptx  12480  txlm  12485  cnmpt21  12497  txswaphmeolem  12526  txswaphmeo  12527  comet  12705  qtopbasss  12727  cnmetdval  12735  remetdval  12745  tgqioo  12753  dvcnp2cntop  12869  dvef  12894  djucllem  13176  pwle2  13364
  Copyright terms: Public domain W3C validator