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

Theorem breq2 3797
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))

Proof of Theorem breq2
StepHypRef Expression
1 opeq2 3579 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21eleq1d 2148 . 2 (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3 df-br 3794 . 2 (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4 df-br 3794 . 2 (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
52, 3, 43bitr4g 221 1 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1285  wcel 1434  cop 3409   class class class wbr 3793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-br 3794
This theorem is referenced by:  breq12  3798  breq2i  3801  breq2d  3805  nbrne1  3810  pocl  4066  swopolem  4068  swopo  4069  sowlin  4083  sotricim  4086  sotritrieq  4088  seex  4098  frind  4115  wetriext  4327  vtoclr  4414  posng  4438  brcog  4530  brcogw  4532  opelcnvg  4543  dfdmf  4556  breldmg  4569  dfrnf  4603  dmcoss  4629  resieq  4650  dfres2  4688  elimag  4702  elreimasng  4721  elimasn  4722  intirr  4741  poirr2  4747  poltletr  4755  dffun6f  4945  dffun4f  4948  fun11  4997  brprcneu  5202  fv3  5229  tz6.12c  5235  relelfvdm  5237  funbrfv  5244  fnbrfvb  5246  funfvdm2f  5270  fndmdif  5304  dff3im  5344  fmptco  5362  foeqcnvco  5461  isorel  5479  isocnv  5482  isotr  5487  isopolem  5492  isosolem  5494  f1oiso  5496  f1oiso2  5497  caovordig  5697  caovordg  5699  caovord  5703  caofrss  5766  caoftrn  5767  poxp  5884  tposoprab  5929  ertr  6187  ecopovsym  6268  ecopovtrn  6269  ecopovsymg  6271  ecopovtrng  6272  th3qlem2  6275  domeng  6299  eqeng  6313  snfig  6359  nneneq  6392  nnfi  6407  ssfilem  6410  domfiexmid  6413  diffitest  6421  findcard  6422  findcard2  6423  findcard2s  6424  diffisn  6427  unsnfi  6439  supmoti  6465  eqsupti  6468  supubti  6471  suplubti  6472  suplub2ti  6473  supmaxti  6476  supsnti  6477  isotilem  6478  isoti  6479  supisolem  6480  supisoex  6481  cardcl  6509  isnumi  6510  cardval3ex  6513  nqtri3or  6648  ltsonq  6650  ltanqg  6652  ltmnqg  6653  ltexnqq  6660  nsmallnqq  6664  subhalfnqq  6666  ltbtwnnqq  6667  prarloclemarch2  6671  nqnq0pi  6690  prcdnql  6736  prcunqu  6737  prnminu  6741  genpcdl  6771  genprndl  6773  genprndu  6774  genpdisj  6775  nqprm  6794  nqprrnd  6795  nqprdisj  6796  nqprloc  6797  nqprlu  6799  nqprl  6803  addnqprlemru  6810  addnqprlemfl  6811  addnqprlemfu  6812  mulnqprlemru  6826  mulnqprlemfl  6827  mulnqprlemfu  6828  1idpru  6843  ltnqpr  6845  ltnqpri  6846  prplnqu  6872  recexprlemelu  6875  recexprlemm  6876  recexprlemloc  6883  recexprlem1ssl  6885  recexprlemss1u  6888  cauappcvgprlemm  6897  cauappcvgprlemopu  6900  cauappcvgprlemupu  6901  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem2  6912  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemopu  6923  caucvgprlemupu  6924  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemcl  6928  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem2  6932  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnbj  6945  caucvgprprlemmu  6947  caucvgprprlemexbt  6958  caucvgprprlemaddq  6960  caucvgprprlem1  6961  caucvgprprlem2  6962  lttrsr  7001  ltsosr  7003  ltasrg  7009  recexgt0sr  7012  mulgt0sr  7016  aptisr  7017  mulextsr1  7019  srpospr  7021  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  caucvgsr  7040  axprecex  7108  axpre-ltwlin  7111  axpre-lttrn  7112  axpre-apti  7113  axpre-ltadd  7114  axpre-mulgt0  7115  axpre-mulext  7116  axcaucvglemcau  7126  axcaucvglemres  7127  axcaucvg  7128  ltxrlt  7245  lttri3  7258  ltne  7263  eqle  7269  reapti  7746  apreim  7770  squeeze0  8049  lbreu  8090  lble  8092  suprleubex  8099  nnge1  8129  nn2ge  8138  nn1gt1  8139  nnsub  8144  nominpos  8335  nn0ge0  8380  elnnnn0b  8399  nn0ge2m1nn  8415  zdclt  8506  suprzclex  8526  peano2uz2  8535  peano5uzti  8536  dfuzi  8538  uzind  8539  uzind3  8541  eluz1  8704  uzind4  8757  indstr  8762  supinfneg  8764  infsupneg  8765  indstr2  8777  ublbneg  8779  elrp  8817  mnfltxr  8937  nn0pnfge0  8942  xrltnsym  8944  xrlttr  8946  xrltso  8947  xrlttri3  8948  xrltne  8959  ngtmnft  8961  xrrebnd  8962  z2ge  8969  xltnegi  8978  ixxval  8995  elixx1  8996  elioo2  9020  iccid  9024  iccsupr  9065  repos  9069  fzval  9107  elfz1  9110  fzm1  9193  exbtwnzlemstep  9334  exbtwnzlemex  9336  qbtwnre  9343  qbtwnxr  9344  flval  9354  apbtwnz  9356  modqid2  9433  modqmuladdnn0  9450  serige0  9570  expival  9575  expge0  9609  expge1  9610  facdiv  9762  facwordi  9764  sizeinf  9802  sizeennn  9804  sizeunlem  9828  ovshftex  9845  shftfibg  9846  shftfib  9849  shftfn  9850  2shfti  9857  sqrt0rlem  10027  resqrexlemex  10049  rsqrmo  10051  resqrtcl  10053  rersqrtthlem  10054  sqrtsq  10068  cau3lem  10138  caubnd2  10141  maxleim  10229  maxabslemval  10232  maxleast  10237  maxleb  10240  fimaxre2  10247  minmax  10250  climi  10264  climeu  10273  climmo  10275  2clim  10278  addcn2  10287  mulcn2  10289  cn1lem  10290  dvdsabsb  10359  0dvds  10360  alzdvds  10399  dvdsext  10400  fzo0dvdseq  10402  2tp1odd  10428  2teven  10431  divalglemnn  10462  divalglemeunn  10465  divalglemeuneg  10467  zsupcllemstep  10485  gcdval  10495  gcddvds  10499  bezoutlemstep  10530  bezoutlemmain  10531  bezoutlemex  10534  bezoutlemeu  10540  bezoutlemsup  10542  dfgcd3  10543  bezout  10544  dvdsgcd  10545  dfgcd2  10547  dvdssq  10564  lcmval  10589  lcmcllem  10593  dvdslcm  10595  lcmledvds  10596  lcmgcdlem  10603  lcmdvds  10605  coprmgcdb  10614  coprmdvds2  10619  cncongr1  10629  cncongr2  10630  isprm  10635  dvdsnprmd  10651  dvdsprm  10662  exprmfct  10663  isprm6  10670  prmexpb  10674  prmfac1  10675  rpexp  10676  sqrt2irr  10685  oddpwdclemdc  10695  oddpwdc  10696  sqpweven  10697  2sqpwodd  10698  sqne2sq  10699  oddennn  10703  evenennn  10704
  Copyright terms: Public domain W3C validator