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

Theorem breq1 3939
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )

Proof of Theorem breq1
StepHypRef Expression
1 opeq1 3712 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2209 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 3937 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 3937 . 2  |-  ( B R C  <->  <. B ,  C >.  e.  R )
52, 3, 43bitr4g 222 1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1332    e. wcel 1481   <.cop 3534   class class class wbr 3936
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-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
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-v 2691  df-un 3079  df-sn 3537  df-pr 3538  df-op 3540  df-br 3937
This theorem is referenced by:  breq12  3941  breq1i  3943  breq1d  3946  nbrne2  3955  brab1  3982  pocl  4232  swopolem  4234  swopo  4235  issod  4248  sowlin  4249  sotritrieq  4254  frirrg  4279  wetriext  4498  vtoclr  4594  brcog  4713  brcogw  4715  opelcnvg  4726  dfdmf  4739  eldmg  4741  dfrnf  4787  dfres2  4878  imasng  4911  coi1  5061  dffun6f  5143  funmo  5145  fun11  5197  fveq2  5428  funfveu  5441  sefvex  5449  nfunsn  5462  fvmptss2  5503  f1ompt  5578  fmptco  5593  dff13  5676  foeqcnvco  5698  isorel  5716  isocnv  5719  isotr  5724  isoini  5726  isopolem  5730  isosolem  5732  f1oiso  5734  f1oiso2  5735  caovordig  5943  caovordg  5945  caovord3d  5948  caovord  5949  caovord3  5951  caofrss  6013  caoftrn  6014  poxp  6136  brtpos2  6155  rntpos  6161  tpostpos  6168  ertr  6451  ecopovsym  6532  ecopovtrn  6533  ecopovsymg  6535  ecopovtrng  6536  th3qlem2  6539  isfi  6662  en0  6696  en1  6700  en1bg  6701  endisj  6725  xpcomco  6727  dom0  6739  ssenen  6752  nneneq  6758  domfiexmid  6779  findcard  6789  findcard2  6790  findcard2s  6791  isinfinf  6798  tridc  6800  fimax2gtrilemstep  6801  fimax2gtri  6802  fiintim  6824  fisseneq  6827  en1eqsnbi  6844  isbth  6862  supmoti  6887  eqsupti  6890  supubti  6893  suplubti  6894  supsnti  6899  isotilem  6900  isoti  6901  supisolem  6902  supisoex  6903  infminti  6921  isnumi  7054  cardval3ex  7057  oncardval  7058  cardonle  7059  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  nqtri3or  7227  ltsonq  7229  ltanqg  7231  ltmnqg  7232  ltexnqq  7239  subhalfnqq  7245  ltbtwnnqq  7246  archnqq  7248  nqnq0pi  7269  prcdnql  7315  prcunqu  7316  prnmaxl  7319  genpcuu  7351  genprndl  7352  genprndu  7353  nqprm  7373  nqprrnd  7374  nqprdisj  7375  nqprloc  7376  nqpru  7383  addnqprlemrl  7388  addnqprlemfl  7390  addnqprlemfu  7391  prmuloc2  7398  mulnqprlemrl  7404  mulnqprlemfl  7406  mulnqprlemfu  7407  1idprl  7421  ltnqpr  7424  ltnqpri  7425  prplnqu  7451  recexprlemell  7453  recexprlemm  7455  recexprlemdisj  7461  recexprlemloc  7462  recexprlem1ssu  7465  recexprlemss1l  7466  aptiprlemu  7471  archpr  7474  cauappcvgprlemm  7476  cauappcvgprlemladdfl  7486  cauappcvgprlem2  7491  cauappcvgpr  7493  caucvgprlemnkj  7497  caucvgprlemnbj  7498  caucvgprlemcl  7507  caucvgprlem2  7511  caucvgpr  7513  caucvgprprlemelu  7517  caucvgprprlemcbv  7518  caucvgprprlemval  7519  caucvgprprlemnbj  7524  caucvgprprlemmu  7526  caucvgprprlemopu  7530  caucvgprprlemexbt  7537  caucvgprprlemaddq  7539  caucvgprprlem1  7540  caucvgprprlem2  7541  caucvgprpr  7543  suplocexprlemmu  7549  suplocexprlemloc  7552  suplocexpr  7556  lttrsr  7593  ltsosr  7595  1ne0sr  7597  ltasrg  7601  aptisr  7610  mulextsr1  7612  archsr  7613  caucvgsrlemgt1  7626  caucvgsrlemoffres  7631  caucvgsr  7633  suplocsrlemb  7637  suplocsrlempr  7638  suplocsrlem  7639  axpre-ltwlin  7714  axpre-lttrn  7715  axpre-apti  7716  axpre-ltadd  7717  axpre-mulext  7719  axcaucvglemcau  7729  axcaucvglemres  7730  axcaucvg  7731  axpre-suploclemres  7732  axpre-suploc  7733  ltxrlt  7853  lttri3  7867  ltordlem  8267  lt0ne0d  8298  reapti  8364  apreim  8388  apsscn  8432  recexap  8437  lbreu  8726  lble  8728  suprleubex  8735  sup3exmid  8738  nnsub  8782  nominpos  8980  nn0n0n1ge2b  9153  zextle  9165  fzind  9189  btwnz  9193  uzval  9351  supinfneg  9416  infsupneg  9417  ublbneg  9431  lbzbi  9434  qreccl  9460  xrltnsym  9608  xrlttr  9610  xrltso  9611  xrlttri3  9612  nltpnft  9626  npnflt  9627  xrrebnd  9631  xltnegi  9647  xnn0lenn0nn0  9677  xsubge0  9693  xlesubadd  9695  xleaddadd  9699  ixxval  9708  elixx1  9709  elioo2  9733  iccid  9737  fzval  9822  elfz1  9825  qtri3or  10050  exbtwnzlemstep  10055  exbtwnzlemshrink  10056  exbtwnzlemex  10057  exbtwnz  10058  rebtwn2zlemstep  10060  rebtwn2zlemshrink  10061  rebtwn2z  10062  qbtwnre  10064  qbtwnxr  10065  flval  10075  flqlelt  10079  flqbi  10093  flqeqceilz  10121  modqid2  10154  seq3f1olemqsum  10303  seq3f1oleml  10306  seq3f1o  10307  expcl2lemap  10335  expclzaplem  10347  expclzap  10348  expap0i  10355  hashinfuni  10554  hashennnuni  10556  hashunlem  10581  zfz1isolemiso  10613  zfz1isolem1  10614  zfz1iso  10615  absle  10892  maxleast  11016  rexanre  11023  rexico  11024  fimaxre2  11029  minmax  11032  xrmaxltsup  11058  xrminmax  11065  climshft  11104  reccn2ap  11113  summodclem3  11180  summodclem2a  11181  summodc  11183  zsumdc  11184  fsum3  11187  fsum3cvg3  11196  fsumcl2lem  11198  fsumadd  11206  sumsnf  11209  fsummulc2  11248  isumlessdc  11296  cvgratz  11332  mertenslemi1  11335  ntrivcvgap0  11349  prodmodclem3  11375  prodmodclem2a  11376  prodmodc  11378  zproddc  11379  absdvdsb  11545  zdvdsdc  11548  dvdsabseq  11579  dvdsdivcl  11582  dvdsext  11587  divalglemnn  11649  divalglemeunn  11652  divalglemeuneg  11654  divalgmod  11658  ndvdssub  11661  zsupcllemstep  11672  gcdsupex  11680  gcdsupcl  11681  gcddvds  11686  dvdslegcd  11687  bezoutlemmain  11720  bezoutlemex  11723  bezoutlemzz  11724  bezoutlemmo  11728  bezoutlemeu  11729  bezoutlemle  11730  bezoutlemsup  11731  dfgcd3  11732  dfgcd2  11736  gcdzeq  11744  dvdssq  11753  nn0seqcvgd  11756  algcvgblem  11764  lcmval  11778  lcmdvds  11794  lcmgcdeq  11798  coprmgcdb  11803  ncoprmgcdne1b  11804  coprmdvds1  11806  1nprm  11829  1idssfct  11830  isprm2lem  11831  isprm2  11832  dvdsprime  11837  nprm  11838  3prm  11843  dvdsprm  11851  exprmfct  11852  coprm  11856  sqrt2irr  11874  exmidunben  11973  ssblex  12637  comet  12705  bdmopn  12710  reopnap  12744  divcnap  12761  cdivcncfap  12793  cnopnap  12800  dedekindeulemuub  12801  dedekindeulemloc  12803  dedekindeulemlu  12805  dedekindeulemeu  12806  dedekindeu  12807  suplociccreex  12808  dedekindicclemuub  12810  dedekindicclemloc  12812  dedekindicclemlu  12814  dedekindicclemeu  12815  dedekindicclemicc  12816  dedekindicc  12817  ivthinclemlopn  12820  ivthinclemlr  12821  ivthinclemuopn  12822  ivthinclemur  12823  ivthinclemloc  12825  ivthinc  12827  limcdifap  12837  limcimolemlt  12839  limccoap  12853  dvlemap  12855  dvidlemap  12866  dvcnp2cntop  12869  dvaddxxbr  12871  dvmulxxbr  12872  dvcoapbr  12877  dvcjbr  12878  dvrecap  12883  dveflem  12893  logltb  13001  2irrexpqap  13101  pw1nct  13369  sbthom  13394  trilpo  13409  trirec0  13410  dcapncf  13421  neapmkv  13423
  Copyright terms: Public domain W3C validator