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

Theorem breq2 3879
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 3653 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21eleq1d 2168 . 2 (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3 df-br 3876 . 2 (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4 df-br 3876 . 2 (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
52, 3, 43bitr4g 222 1 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1299  wcel 1448  cop 3477   class class class wbr 3875
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-br 3876
This theorem is referenced by:  breq12  3880  breq2i  3883  breq2d  3887  nbrne1  3892  pocl  4163  swopolem  4165  swopo  4166  sowlin  4180  sotricim  4183  sotritrieq  4185  seex  4195  frind  4212  wetriext  4429  vtoclr  4525  posng  4549  brcog  4644  brcogw  4646  opelcnvg  4657  dfdmf  4670  breldmg  4683  dfrnf  4718  dmcoss  4744  resieq  4765  dfres2  4807  elimag  4821  elreimasng  4841  elimasn  4842  intirr  4861  poirr2  4867  poltletr  4875  dffun6f  5072  dffun4f  5075  fun11  5126  brprcneu  5346  fv3  5376  tz6.12c  5383  relelfvdm  5385  funbrfv  5392  fnbrfvb  5394  funfvdm2f  5418  fndmdif  5457  dff3im  5497  fmptco  5518  foeqcnvco  5623  isorel  5641  isocnv  5644  isotr  5649  isopolem  5655  isosolem  5657  f1oiso  5659  f1oiso2  5660  caovordig  5868  caovordg  5870  caovord  5874  caofrss  5937  caoftrn  5938  poxp  6059  tposoprab  6107  ertr  6374  ecopovsym  6455  ecopovtrn  6456  ecopovsymg  6458  ecopovtrng  6459  th3qlem2  6462  domeng  6576  eqeng  6590  snfig  6638  nneneq  6680  nnfi  6695  ssfilem  6698  domfiexmid  6701  dif1enen  6703  diffitest  6710  findcard  6711  findcard2  6712  findcard2s  6713  diffisn  6716  tridc  6722  fimax2gtrilemstep  6723  inffiexmid  6729  unsnfi  6736  fiintim  6746  fisseneq  6749  isbth  6783  supmoti  6795  eqsupti  6798  supubti  6801  suplubti  6802  suplub2ti  6803  supmaxti  6806  supsnti  6807  isotilem  6808  isoti  6809  supisolem  6810  supisoex  6811  cardcl  6948  isnumi  6949  cardval3ex  6952  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  nqtri3or  7105  ltsonq  7107  ltanqg  7109  ltmnqg  7110  ltexnqq  7117  nsmallnqq  7121  subhalfnqq  7123  ltbtwnnqq  7124  prarloclemarch2  7128  nqnq0pi  7147  prcdnql  7193  prcunqu  7194  prnminu  7198  genpcdl  7228  genprndl  7230  genprndu  7231  genpdisj  7232  nqprm  7251  nqprrnd  7252  nqprdisj  7253  nqprloc  7254  nqprlu  7256  nqprl  7260  addnqprlemru  7267  addnqprlemfl  7268  addnqprlemfu  7269  mulnqprlemru  7283  mulnqprlemfl  7284  mulnqprlemfu  7285  1idpru  7300  ltnqpr  7302  ltnqpri  7303  prplnqu  7329  recexprlemelu  7332  recexprlemm  7333  recexprlemloc  7340  recexprlem1ssl  7342  recexprlemss1u  7345  cauappcvgprlemm  7354  cauappcvgprlemopu  7357  cauappcvgprlemupu  7358  cauappcvgprlemdisj  7360  cauappcvgprlemloc  7361  cauappcvgprlemladdfu  7363  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgprlem2  7369  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemm  7377  caucvgprlemopu  7380  caucvgprlemupu  7381  caucvgprlemdisj  7383  caucvgprlemloc  7384  caucvgprlemcl  7385  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  caucvgprlem2  7389  caucvgprprlemelu  7395  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemnbj  7402  caucvgprprlemmu  7404  caucvgprprlemexbt  7415  caucvgprprlemaddq  7417  caucvgprprlem1  7418  caucvgprprlem2  7419  lttrsr  7458  ltsosr  7460  ltasrg  7466  recexgt0sr  7469  mulgt0sr  7473  aptisr  7474  mulextsr1  7476  srpospr  7478  caucvgsrlemgt1  7490  caucvgsrlemoffres  7495  caucvgsr  7497  axprecex  7565  axpre-ltwlin  7568  axpre-lttrn  7569  axpre-apti  7570  axpre-ltadd  7571  axpre-mulgt0  7572  axpre-mulext  7573  axcaucvglemcau  7583  axcaucvglemres  7584  axcaucvg  7585  ltxrlt  7702  lttri3  7715  ltne  7720  eqle  7726  ltordlem  8111  reapti  8207  apreim  8231  squeeze0  8520  lbreu  8561  lble  8563  suprleubex  8570  sup3exmid  8573  nnge1  8601  nn2ge  8611  nn1gt1  8612  nnsub  8617  nominpos  8809  nn0ge0  8854  elnnnn0b  8873  nn0ge2m1nn  8889  zdclt  8980  suprzclex  9001  peano2uz2  9010  peano5uzti  9011  dfuzi  9013  uzind  9014  uzind3  9016  eluz1  9180  uzind4  9233  indstr  9238  supinfneg  9240  infsupneg  9241  indstr2  9253  ublbneg  9255  elrp  9293  mnfltxr  9413  nn0pnfge0  9418  xrltnsym  9420  xrlttr  9422  xrltso  9423  xrlttri3  9424  xrltne  9437  ngtmnft  9441  nmnfgt  9442  xrrebnd  9443  z2ge  9450  xltnegi  9459  xltadd1  9500  xsubge0  9505  xleaddadd  9511  ixxval  9520  elixx1  9521  elioo2  9545  iccid  9549  iccsupr  9590  repos  9594  fzval  9633  elfz1  9636  fzm1  9721  exbtwnzlemstep  9866  exbtwnzlemex  9868  qbtwnre  9875  qbtwnxr  9876  flval  9886  apbtwnz  9888  modqid2  9965  modqmuladdnn0  9982  exp3val  10136  expge0  10170  expge1  10171  facdiv  10325  facwordi  10327  hashinfom  10365  hashennn  10367  hashunlem  10391  zfz1iso  10425  ovshftex  10432  shftfibg  10433  shftfib  10436  shftfn  10437  2shfti  10444  sqrt0rlem  10615  resqrexlemex  10637  rsqrmo  10639  resqrtcl  10641  rersqrtthlem  10642  sqrtsq  10656  cau3lem  10726  caubnd2  10729  maxleim  10817  maxabslemval  10820  maxleast  10825  maxleb  10828  fimaxre2  10837  minmax  10840  xrmaxleim  10852  xrmaxiflemval  10858  xrmaxaddlem  10868  xrminmax  10873  xrbdtri  10884  climi  10895  climeu  10904  climmo  10906  2clim  10909  addcn2  10918  mulcn2  10920  reccn2ap  10921  cn1lem  10922  summodc  10991  zsumdc  10992  fsum3  10995  cvgratz  11140  dvdsabsb  11307  0dvds  11308  alzdvds  11347  dvdsext  11348  fzo0dvdseq  11350  2tp1odd  11376  2teven  11379  divalglemnn  11410  divalglemeunn  11413  divalglemeuneg  11415  zsupcllemstep  11433  gcdval  11443  gcddvds  11447  bezoutlemstep  11478  bezoutlemmain  11479  bezoutlemex  11482  bezoutlemeu  11488  bezoutlemsup  11490  dfgcd3  11491  bezout  11492  dvdsgcd  11493  dfgcd2  11495  dvdssq  11512  lcmval  11537  lcmcllem  11541  dvdslcm  11543  lcmledvds  11544  lcmgcdlem  11551  lcmdvds  11553  coprmgcdb  11562  coprmdvds2  11567  cncongr1  11577  cncongr2  11578  isprm  11583  dvdsnprmd  11599  dvdsprm  11610  exprmfct  11611  isprm6  11618  prmexpb  11622  prmfac1  11623  rpexp  11624  sqrt2irr  11633  oddpwdclemdc  11643  oddpwdc  11644  sqpweven  11645  2sqpwodd  11646  sqne2sq  11647  oddennn  11697  evenennn  11698  exmidunben  11731  comet  12427  metcnpi  12439  metcnpi2  12440  metcnpi3  12441  cncfi  12478  elcncf1di  12479  mulcncflem  12502  limcimo  12514  eldvap  12524  sbthom  12805  trilpo  12820
  Copyright terms: Public domain W3C validator