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

Theorem breq2 3903
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 3676 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21eleq1d 2186 . 2 (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3 df-br 3900 . 2 (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4 df-br 3900 . 2 (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
52, 3, 43bitr4g 222 1 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1316  wcel 1465  cop 3500   class class class wbr 3899
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900
This theorem is referenced by:  breq12  3904  breq2i  3907  breq2d  3911  nbrne1  3917  brralrspcev  3956  brimralrspcev  3957  pocl  4195  swopolem  4197  swopo  4198  sowlin  4212  sotricim  4215  sotritrieq  4217  seex  4227  frind  4244  wetriext  4461  vtoclr  4557  posng  4581  brcog  4676  brcogw  4678  opelcnvg  4689  dfdmf  4702  breldmg  4715  dfrnf  4750  dmcoss  4778  resieq  4799  dfres2  4841  elimag  4855  elreimasng  4875  elimasn  4876  intirr  4895  poirr2  4901  poltletr  4909  dffun6f  5106  dffun4f  5109  fun11  5160  brprcneu  5382  fv3  5412  tz6.12c  5419  relelfvdm  5421  funbrfv  5428  fnbrfvb  5430  funfvdm2f  5454  fndmdif  5493  dff3im  5533  fmptco  5554  foeqcnvco  5659  isorel  5677  isocnv  5680  isotr  5685  isopolem  5691  isosolem  5693  f1oiso  5695  f1oiso2  5696  caovordig  5904  caovordg  5906  caovord  5910  caofrss  5974  caoftrn  5975  poxp  6097  tposoprab  6145  ertr  6412  ecopovsym  6493  ecopovtrn  6494  ecopovsymg  6496  ecopovtrng  6497  th3qlem2  6500  domeng  6614  eqeng  6628  snfig  6676  nneneq  6719  nnfi  6734  ssfilem  6737  domfiexmid  6740  dif1enen  6742  diffitest  6749  findcard  6750  findcard2  6751  findcard2s  6752  diffisn  6755  tridc  6761  fimax2gtrilemstep  6762  inffiexmid  6768  unsnfi  6775  fiintim  6785  fisseneq  6788  isbth  6823  supmoti  6848  eqsupti  6851  supubti  6854  suplubti  6855  suplub2ti  6856  supmaxti  6859  supsnti  6860  isotilem  6861  isoti  6862  supisolem  6863  supisoex  6864  cardcl  7005  isnumi  7006  cardval3ex  7009  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  nqtri3or  7172  ltsonq  7174  ltanqg  7176  ltmnqg  7177  ltexnqq  7184  nsmallnqq  7188  subhalfnqq  7190  ltbtwnnqq  7191  prarloclemarch2  7195  nqnq0pi  7214  prcdnql  7260  prcunqu  7261  prnminu  7265  genpcdl  7295  genprndl  7297  genprndu  7298  genpdisj  7299  nqprm  7318  nqprrnd  7319  nqprdisj  7320  nqprloc  7321  nqprlu  7323  nqprl  7327  addnqprlemru  7334  addnqprlemfl  7335  addnqprlemfu  7336  mulnqprlemru  7350  mulnqprlemfl  7351  mulnqprlemfu  7352  1idpru  7367  ltnqpr  7369  ltnqpri  7370  prplnqu  7396  recexprlemelu  7399  recexprlemm  7400  recexprlemloc  7407  recexprlem1ssl  7409  recexprlemss1u  7412  cauappcvgprlemm  7421  cauappcvgprlemopu  7424  cauappcvgprlemupu  7425  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdfu  7430  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem2  7436  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemopu  7447  caucvgprlemupu  7448  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemcl  7452  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem2  7456  caucvgprprlemelu  7462  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemnbj  7469  caucvgprprlemmu  7471  caucvgprprlemexbt  7482  caucvgprprlemaddq  7484  caucvgprprlem1  7485  caucvgprprlem2  7486  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  suplocexpr  7501  lttrsr  7538  ltsosr  7540  ltasrg  7546  recexgt0sr  7549  mulgt0sr  7554  aptisr  7555  mulextsr1  7557  srpospr  7559  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  caucvgsr  7578  map2psrprg  7581  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  axprecex  7656  axpre-ltwlin  7659  axpre-lttrn  7660  axpre-apti  7661  axpre-ltadd  7662  axpre-mulgt0  7663  axpre-mulext  7664  axcaucvglemcau  7674  axcaucvglemres  7675  axcaucvg  7676  axpre-suploclemres  7677  axpre-suploc  7678  ltxrlt  7798  lttri3  7812  ltne  7817  eqle  7823  ltordlem  8212  reapti  8309  apreim  8333  squeeze0  8630  lbreu  8671  lble  8673  suprleubex  8680  sup3exmid  8683  nnge1  8711  nn2ge  8721  nn1gt1  8722  nnsub  8727  nominpos  8925  nn0ge0  8970  elnnnn0b  8989  nn0ge2m1nn  9005  zdclt  9096  suprzclex  9117  peano2uz2  9126  peano5uzti  9127  dfuzi  9129  uzind  9130  uzind3  9132  eluz1  9298  uzind4  9351  indstr  9356  supinfneg  9358  infsupneg  9359  indstr2  9371  ublbneg  9373  elrp  9411  mnfltxr  9540  nn0pnfge0  9545  xrltnsym  9547  xrlttr  9549  xrltso  9550  xrlttri3  9551  xrltne  9564  ngtmnft  9568  nmnfgt  9569  xrrebnd  9570  z2ge  9577  xltnegi  9586  xltadd1  9627  xsubge0  9632  xleaddadd  9638  ixxval  9647  elixx1  9648  elioo2  9672  iccid  9676  iccsupr  9717  repos  9721  fzval  9760  elfz1  9763  fzm1  9848  exbtwnzlemstep  9993  exbtwnzlemex  9995  qbtwnre  10002  qbtwnxr  10003  flval  10013  apbtwnz  10015  modqid2  10092  modqmuladdnn0  10109  exp3val  10263  expge0  10297  expge1  10298  facdiv  10452  facwordi  10454  hashinfom  10492  hashennn  10494  hashunlem  10518  zfz1iso  10552  ovshftex  10559  shftfibg  10560  shftfib  10563  shftfn  10564  2shfti  10571  sqrt0rlem  10743  resqrexlemex  10765  rsqrmo  10767  resqrtcl  10769  rersqrtthlem  10770  sqrtsq  10784  cau3lem  10854  caubnd2  10857  maxleim  10945  maxabslemval  10948  maxleast  10953  maxleb  10956  fimaxre2  10966  minmax  10969  xrmaxleim  10981  xrmaxiflemval  10987  xrmaxaddlem  10997  xrminmax  11002  xrbdtri  11013  climi  11024  climeu  11033  climmo  11035  2clim  11038  addcn2  11047  mulcn2  11049  reccn2ap  11050  cn1lem  11051  summodc  11120  zsumdc  11121  fsum3  11124  cvgratz  11269  dvdsabsb  11439  0dvds  11440  alzdvds  11479  dvdsext  11480  fzo0dvdseq  11482  2tp1odd  11508  2teven  11511  divalglemnn  11542  divalglemeunn  11545  divalglemeuneg  11547  zsupcllemstep  11565  gcdval  11575  gcddvds  11579  bezoutlemstep  11612  bezoutlemmain  11613  bezoutlemex  11616  bezoutlemeu  11622  bezoutlemsup  11624  dfgcd3  11625  bezout  11626  dvdsgcd  11627  dfgcd2  11629  dvdssq  11646  lcmval  11671  lcmcllem  11675  dvdslcm  11677  lcmledvds  11678  lcmgcdlem  11685  lcmdvds  11687  coprmgcdb  11696  coprmdvds2  11701  cncongr1  11711  cncongr2  11712  isprm  11717  dvdsnprmd  11733  dvdsprm  11744  exprmfct  11745  isprm6  11752  prmexpb  11756  prmfac1  11757  rpexp  11758  sqrt2irr  11767  oddpwdclemdc  11778  oddpwdc  11779  sqpweven  11780  2sqpwodd  11781  sqne2sq  11782  oddennn  11832  evenennn  11833  exmidunben  11866  comet  12595  metcnpi  12611  metcnpi2  12612  metcnpi3  12613  addcncntoplem  12647  cncfi  12661  elcncf1di  12662  mulcncflem  12686  dedekindeulemuub  12691  dedekindeulemloc  12693  dedekindeulemlu  12695  dedekindeulemeu  12696  dedekindeu  12697  suplociccreex  12698  suplociccex  12699  dedekindicclemuub  12700  dedekindicclemloc  12702  dedekindicclemlu  12704  dedekindicclemeu  12705  dedekindicclemicc  12706  dedekindicc  12707  ivthinclemlopn  12710  ivthinclemlr  12711  ivthinclemuopn  12712  ivthinclemur  12713  ivthinclemloc  12715  ivthinc  12717  limcimo  12730  cnplimclemr  12734  limccnp2lem  12741  limccoap  12743  eldvap  12747  sbthom  13148  trilpo  13163
  Copyright terms: Public domain W3C validator