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

Theorem breq2 3940
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 3713 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21eleq1d 2209 . 2 (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3 df-br 3937 . 2 (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4 df-br 3937 . 2 (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
52, 3, 43bitr4g 222 1 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1332  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  breq2i  3944  breq2d  3948  nbrne1  3954  brralrspcev  3993  brimralrspcev  3994  pocl  4232  swopolem  4234  swopo  4235  sowlin  4249  sotricim  4252  sotritrieq  4254  seex  4264  frind  4281  wetriext  4498  vtoclr  4594  posng  4618  brcog  4713  brcogw  4715  opelcnvg  4726  dfdmf  4739  breldmg  4752  dfrnf  4787  dmcoss  4815  resieq  4836  dfres2  4878  elimag  4892  elreimasng  4912  elimasn  4913  intirr  4932  poirr2  4938  poltletr  4946  dffun6f  5143  dffun4f  5146  fun11  5197  brprcneu  5421  fv3  5451  tz6.12c  5458  relelfvdm  5460  funbrfv  5467  fnbrfvb  5469  funfvdm2f  5493  fndmdif  5532  dff3im  5572  fmptco  5593  foeqcnvco  5698  isorel  5716  isocnv  5719  isotr  5724  isopolem  5730  isosolem  5732  f1oiso  5734  f1oiso2  5735  caovordig  5943  caovordg  5945  caovord  5949  caofrss  6013  caoftrn  6014  poxp  6136  tposoprab  6184  ertr  6451  ecopovsym  6532  ecopovtrn  6533  ecopovsymg  6535  ecopovtrng  6536  th3qlem2  6539  domeng  6653  eqeng  6667  snfig  6715  nneneq  6758  nnfi  6773  ssfilem  6776  domfiexmid  6779  dif1enen  6781  diffitest  6788  findcard  6789  findcard2  6790  findcard2s  6791  diffisn  6794  tridc  6800  fimax2gtrilemstep  6801  inffiexmid  6807  unsnfi  6814  fiintim  6824  fisseneq  6827  isbth  6862  supmoti  6887  eqsupti  6890  supubti  6893  suplubti  6894  suplub2ti  6895  supmaxti  6898  supsnti  6899  isotilem  6900  isoti  6901  supisolem  6902  supisoex  6903  cardcl  7053  isnumi  7054  cardval3ex  7057  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  nqtri3or  7227  ltsonq  7229  ltanqg  7231  ltmnqg  7232  ltexnqq  7239  nsmallnqq  7243  subhalfnqq  7245  ltbtwnnqq  7246  prarloclemarch2  7250  nqnq0pi  7269  prcdnql  7315  prcunqu  7316  prnminu  7320  genpcdl  7350  genprndl  7352  genprndu  7353  genpdisj  7354  nqprm  7373  nqprrnd  7374  nqprdisj  7375  nqprloc  7376  nqprlu  7378  nqprl  7382  addnqprlemru  7389  addnqprlemfl  7390  addnqprlemfu  7391  mulnqprlemru  7405  mulnqprlemfl  7406  mulnqprlemfu  7407  1idpru  7422  ltnqpr  7424  ltnqpri  7425  prplnqu  7451  recexprlemelu  7454  recexprlemm  7455  recexprlemloc  7462  recexprlem1ssl  7464  recexprlemss1u  7467  cauappcvgprlemm  7476  cauappcvgprlemopu  7479  cauappcvgprlemupu  7480  cauappcvgprlemdisj  7482  cauappcvgprlemloc  7483  cauappcvgprlemladdfu  7485  cauappcvgprlemladdru  7487  cauappcvgprlemladdrl  7488  cauappcvgprlem2  7491  caucvgprlemnkj  7497  caucvgprlemnbj  7498  caucvgprlemm  7499  caucvgprlemopu  7502  caucvgprlemupu  7503  caucvgprlemdisj  7505  caucvgprlemloc  7506  caucvgprlemcl  7507  caucvgprlemladdfu  7508  caucvgprlemladdrl  7509  caucvgprlem2  7511  caucvgprprlemelu  7517  caucvgprprlemcbv  7518  caucvgprprlemval  7519  caucvgprprlemnbj  7524  caucvgprprlemmu  7526  caucvgprprlemexbt  7537  caucvgprprlemaddq  7539  caucvgprprlem1  7540  caucvgprprlem2  7541  suplocexprlemmu  7549  suplocexprlemru  7550  suplocexprlemdisj  7551  suplocexprlemloc  7552  suplocexprlemub  7554  suplocexpr  7556  lttrsr  7593  ltsosr  7595  ltasrg  7601  recexgt0sr  7604  mulgt0sr  7609  aptisr  7610  mulextsr1  7612  srpospr  7614  caucvgsrlemgt1  7626  caucvgsrlemoffres  7631  caucvgsr  7633  map2psrprg  7636  suplocsrlemb  7637  suplocsrlempr  7638  suplocsrlem  7639  axprecex  7711  axpre-ltwlin  7714  axpre-lttrn  7715  axpre-apti  7716  axpre-ltadd  7717  axpre-mulgt0  7718  axpre-mulext  7719  axcaucvglemcau  7729  axcaucvglemres  7730  axcaucvg  7731  axpre-suploclemres  7732  axpre-suploc  7733  ltxrlt  7853  lttri3  7867  ltne  7872  eqle  7878  ltordlem  8267  reapti  8364  apreim  8388  squeeze0  8685  lbreu  8726  lble  8728  suprleubex  8735  sup3exmid  8738  nnge1  8766  nn2ge  8776  nn1gt1  8777  nnsub  8782  nominpos  8980  nn0ge0  9025  elnnnn0b  9044  nn0ge2m1nn  9060  zdclt  9151  suprzclex  9172  peano2uz2  9181  peano5uzti  9182  dfuzi  9184  uzind  9185  uzind3  9187  eluz1  9353  uzind4  9409  indstr  9414  supinfneg  9416  infsupneg  9417  indstr2  9429  ublbneg  9431  elpq  9466  elpqb  9467  elrp  9471  mnfltxr  9601  nn0pnfge0  9606  xrltnsym  9608  xrlttr  9610  xrltso  9611  xrlttri3  9612  xrltne  9625  ngtmnft  9629  nmnfgt  9630  xrrebnd  9631  z2ge  9638  xltnegi  9647  xltadd1  9688  xsubge0  9693  xleaddadd  9699  ixxval  9708  elixx1  9709  elioo2  9733  iccid  9737  iccsupr  9778  repos  9782  fzval  9822  elfz1  9825  fzm1  9910  exbtwnzlemstep  10055  exbtwnzlemex  10057  qbtwnre  10064  qbtwnxr  10065  flval  10075  apbtwnz  10077  modqid2  10154  modqmuladdnn0  10171  exp3val  10325  expge0  10359  expge1  10360  facdiv  10515  facwordi  10517  hashinfom  10555  hashennn  10557  hashunlem  10581  zfz1iso  10615  ovshftex  10622  shftfibg  10623  shftfib  10626  shftfn  10627  2shfti  10634  sqrt0rlem  10806  resqrexlemex  10828  rsqrmo  10830  resqrtcl  10832  rersqrtthlem  10833  sqrtsq  10847  cau3lem  10917  caubnd2  10920  maxleim  11008  maxabslemval  11011  maxleast  11016  maxleb  11019  fimaxre2  11029  minmax  11032  xrmaxleim  11044  xrmaxiflemval  11050  xrmaxaddlem  11060  xrminmax  11065  xrbdtri  11076  climi  11087  climeu  11096  climmo  11098  2clim  11101  addcn2  11110  mulcn2  11112  reccn2ap  11113  cn1lem  11114  summodc  11183  zsumdc  11184  fsum3  11187  cvgratz  11332  ntrivcvgap0  11349  prodmodc  11378  zproddc  11379  dvdsabsb  11546  0dvds  11547  alzdvds  11586  dvdsext  11587  fzo0dvdseq  11589  2tp1odd  11615  2teven  11618  divalglemnn  11649  divalglemeunn  11652  divalglemeuneg  11654  zsupcllemstep  11672  gcdval  11682  gcddvds  11686  bezoutlemstep  11719  bezoutlemmain  11720  bezoutlemex  11723  bezoutlemeu  11729  bezoutlemsup  11731  dfgcd3  11732  bezout  11733  dvdsgcd  11734  dfgcd2  11736  dvdssq  11753  lcmval  11778  lcmcllem  11782  dvdslcm  11784  lcmledvds  11785  lcmgcdlem  11792  lcmdvds  11794  coprmgcdb  11803  coprmdvds2  11808  cncongr1  11818  cncongr2  11819  isprm  11824  dvdsnprmd  11840  dvdsprm  11851  exprmfct  11852  isprm6  11859  prmexpb  11863  prmfac1  11864  rpexp  11865  sqrt2irr  11874  oddpwdclemdc  11885  oddpwdc  11886  sqpweven  11887  2sqpwodd  11888  sqne2sq  11889  oddennn  11939  evenennn  11940  exmidunben  11973  comet  12705  metcnpi  12721  metcnpi2  12722  metcnpi3  12723  addcncntoplem  12757  cncfi  12771  elcncf1di  12772  mulcncflem  12796  dedekindeulemuub  12801  dedekindeulemloc  12803  dedekindeulemlu  12805  dedekindeulemeu  12806  dedekindeu  12807  suplociccreex  12808  suplociccex  12809  dedekindicclemuub  12810  dedekindicclemloc  12812  dedekindicclemlu  12814  dedekindicclemeu  12815  dedekindicclemicc  12816  dedekindicc  12817  ivthinclemlopn  12820  ivthinclemlr  12821  ivthinclemuopn  12822  ivthinclemur  12823  ivthinclemloc  12825  ivthinc  12827  limcimo  12840  cnplimclemr  12844  limccnp2lem  12851  limccoap  12853  eldvap  12857  logltb  13001  sbthom  13394  trilpo  13409  trirec0  13410  apdiff  13414  neapmkv  13423
  Copyright terms: Public domain W3C validator