Theorem breq2 3543

Description: Equality theorem for a binary relation.

Assertion

Ref	Expression
breq2	|- (A = B -> (CRA <-> CRB))

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 3378	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	eleq1d 2239	. 2 |- (A = B -> (<.C, A>. e. R <-> <.C, B>. e. R))
3		df-br 3540	. 2 |- (CRA <-> <.C, A>. e. R)
4		df-br 3540	. 2 |- (CRB <-> <.C, B>. e. R)
5	2, 3, 4	3bitr4g 351	1 |- (A = B -> (CRA <-> CRB))

Syntax hints:   -> wi 3   <-> wb 231   = wceq 1615   e. wcel 1617  <.cop 3272   class class class wbr 3539

This theorem is referenced by:  breq12 3544  breq2i 3547  breq2d 3551  nbrne1 3556  pocl 3788  posn 3794  solin 3803  sotric 3806  sotrieq 3807  so 3810  dffr2 3816  frirr 3821  fr2nr 3822  frminex 3824  wereu 3840  fr3nr 4037  dfwe2 4039  vtoclr 4199  vtoclibr 4201  opelco 4291  opelco2g 4293  opelcnvg 4300  dmcoss 4365  resieq 4381  elimag 4419  elimasn 4440  asymref2 4456  intirr 4457  sotri3 4463  dffun3 4574  dffun6f 4577  fun11 4619  fv3 4818  tz6.12c 4825  tz6.12i 4826  funbrfv 4833  fnbrfvbg 4836  funbrfvbg 4841  funfv2f 4857  dffv2 4859  dff3 4919  isorel 5004  isocnv 5006  isotr 5009  isotrALT 5010  isowe 5015  f1oiso 5016  f1oiso2 5017  f1oweALT 5019  caoprord 5121  frxp 5250  poxp 5252  errsym 5532  ertr 5533  errtr 5535  erref 5536  elec 5540  ecopoprsym 5573  ecopoprtrn 5574  th3qlem2 5578  domeng 5643  eqeng 5655  ensymg 5674  snfi 5697  xpdom1g 5710  sbth 5729  xpeng 5813  xpengOLDOLD 5814  xpnum 5815  nneneq 5842  php2 5844  onfin 5849  1sdom 5859  unxpdom 5864  sucxpdom 5866  omsdomnn 5870  isinf 5872  fineqvlem 5873  pssnn 5878  ssnnfi 5879  dif1en 5886  findcard 5887  findcard2 5888  fimax 5890  fisupg 5892  frfi 5895  unfi 5907  unifi 5914  fiint 5916  indexfi 5922  fodomfi 5924  supmo 5939  supub 5943  suplub 5944  fisup2g 5952  supmaxlem 5953  suppr 5955  supsnALT 5957  ordtypelem2 5960  ordtypelem6 5964  ordtypelem7 5965  ordtype 5966  hartogs 5968  onsdom 5969  r111 6050  hta 6162  cardval3 6169  oncardval 6174  cardnueq0 6183  carden2a 6186  sdomsdomcardi 6191  cardlim 6192  cardmin2 6203  dif1cardOLD 6209  alephnbtwn 6222  alephordilem1 6223  omsubsuc 6233  omsubsuc2 6234  omsubsdomlem1 6235  elomsubsd 6241  omsubinit 6246  mappwen 6247  aceq3lem 6251  onssnum 6272  fodomnum 6274  alephnbtwn2 6275  alephsucdom 6276  cardaleph 6280  cdaeng 6312  cdainf 6325  cfflb 6346  domtriomlem 6365  domtriomlemOLD 6366  domtriomlemOLDOLD 6369  dominf 6371  numth2 6431  zorn2lem2 6436  zorn2lem7 6441  zorn2 6443  axdclem 6445  axdc 6447  fodomg 6449  brdom7disj 6454  brdom6disj 6455  unidomg 6460  cardval 6464  carden 6470  unxpdomOLD 6486  cardlimOLD 6492  cardmin 6500  ficard 6502  alephnbtwnOLD 6509  alephordilem1OLD 6513  cardalephOLD 6520  alephval2 6521  dominfac 6522  cfpwsdom 6528  ltpiord 6610  indpi 6629  ltsopq 6670  ltapq 6671  ltmpq 6672  ltexpq 6675  nsmallpq 6678  ltbtwnpq 6679  ltrpq 6680  prcdpq 6692  genpcd 6704  genpnmax 6705  prlem934b 6733  ltaddpr2 6736  ltexprlem4 6740  reclem3pr 6753  supexpr 6758  ltsosr 6798  ltasr 6804  recexsrlem 6807  mulgt0sr 6809  map2psrpr 6815  suppsrlem 6816  suppsr 6817  suppsr2 6818  suppsr3 6819  supsrlem5 6824  supsrlem6 6825  supre 6855  ltsor 6856  axpre-ltadd 6882  axpre-mulgt0 6883  ltxr 6956  ltletr 6985  letr 6986  mnfltxr 7006  xrltnsym 7011  xrlttri 7013  xrlttr 7014  xrltletr 7024  xrletr 7025  ngtmnft 7028  eqle 7032  readdcani 7070  gt0ne0 7246  ltadd1 7247  leadd1 7249  ltsubadd 7251  lesubadd 7253  lt2add 7267  le2add 7268  ltneg 7279  leneg 7281  lesub0 7302  mulge0 7303  mulge0OLD 7304  elimgt0 7420  elimge0 7421  prodgt0 7437  prodge0 7439  ltmul1 7441  ltdiv1 7466  ltdiv1OLD 7467  ltmuldiv 7480  ltmuldivOLD 7481  ltreci 7497  ltrec 7502  lerec 7503  lt2msq 7504  le2msq 7521  posexi 7526  xrltmin 7532  lemin 7539  squeeze0 7542  nn2ge 7560  nnge1 7561  nnleltp1 7573  nnsubi 7575  nnsub 7576  halfpos 7668  nominpos 7676  elrp 7679  lbreu 7702  lble 7704  lbinfm 7705  sup2 7708  infm3 7711  suprleub 7718  infmsup 7729  infmrcl 7730  nnunb 7731  xrsupexmnf 7735  xrsupsslem 7737  xrinfmsslem 7738  xrub 7741  supxr 7742  supxrre 7744  supxrpnf 7749  supxrunb1 7750  supxrunb2 7751  lt0nnn0 7778  nn0ltp1le 7789  elnnz1 7817  nn0sub 7823  zltp1le 7844  z2ge 7855  peano2uz2 7868  dfuzi 7869  uzind 7872  uzind3 7874  uzindOLD 7875  uzind3OLD 7876  uzwo4OLD 7877  uzwo5OLD 7878  uzwo3lem2 7887  uzwo3 7888  zmin 7889  zmax 7890  zbtwnre 7891  rebtwnz 7892  qbtwnre 7917  qbtwnxr 7918  flval 7922  flval2 7936  flval3 7937  modid2 7971  monoord 7981  iooval 7991  iocval 8000  icoval 8001  iccval 8002  elioo1 8003  elioo2 8004  elioc1 8006  elico1 8007  elicc1 8008  iccsupr 8025  repos 8026  icoun 8040  snunioo 8042  eluz1 8048  uzind4 8080  uzwo 8085  uzwoOLD 8086  nnwof 8089  indstr2 8099  ublbneg 8106  suprzcl 8111  fzval 8114  elfz1 8115  fzsuc 8155  fsequb 8187  om2uzuzi 8193  om2uzrani 8196  uzrdginii 8200  uzrdginip1i 8202  seqzval 8274  seqz1 8281  sq11 8374  sqrval 8421  sqr0 8422  sqrlem4 8426  sqrlem6 8428  sqrlem12 8434  sqrlem13 8435  sqrlem20 8442  sqrlem21 8443  sqrlem22 8444  sqrlem24 8446  sqrgt0ii 8447  sqrlem26 8448  sqrcl 8460  sqrgt0 8461  sqrge0 8462  sqrle 8463  sqr00 8464  sqrsq 8472  sqsqr 8473  sqr2irrlem1 8474  sqr2irrlem2 8475  sqr2irr 8479  absid 8613  abslt 8632  absle 8633  abs3lem 8660  seq1bndi 8663  cau3ii 8667  cau3iri 8668  cvg2i 8675  caubndi 8679  facdiv 8695  facwordi 8697  bcval 8711  bcpasc2 8721  bccl2 8724  hashgval 8732  dffsum 8770  clm4lei 8853  clmi1i 8858  climuni 8871  climeu 8872  2climnn 8874  2climnn0 8875  climshfti 8876  iserzshft2i 8879  climrecl 8882  climge0 8884  climaddlem3 8888  climmullem8 8899  iserzex 8907  climcmplem 8909  iserzexi 8918  climubii 8925  climsupi 8927  climcaui 8928  caucvglem2 8930  caucvglem6 8934  caucvgi 8935  caucvg2i 8937  caucvg3lem 8938  caucvg3 8940  serzf0i 8941  ser1cmp2i 8949  cvgcmp2lem 8952  cvgcmpubi 8958  cvgcmp3cei 8960  cvgcmp3cetlem1 8961  cvgcmp3cetlem2 8962  isumclimtfi 8968  isumspliti 8989  supcvglem 8992  supcvg 8993  supcvglemOLD 8994  infcvglem1OLD 8998  expcnvlem3 9006  expcnvlem5 9008  geoisum1c 9023  cvgratlem1ALT 9025  cvgratlem1 9028  cvgratlem4 9031  elcncf1di 9048  ivthlem2 9060  efseq1ex 9084  efseq0ex 9089  efaddlem24 9139  eftlex 9156  eflegeo 9197  efm1legeo 9199  efcnlem4 9203  efcn 9204  reeff1olem2 9206  reefiso 9209  acdc3 9271  acdc2 9275  acdc5 9278  acdc 9280  rpnnen1lem1 9289  rpnnen1lem2 9290  rpnnen1lem4 9292  rpnnen1lem5 9293  rpnnen2lem5 9299  rpnnen 9307  ruclem4 9312  ruclem33 9341  ruclem35 9343  ruclem36 9344  infxpidmlem2OLD 9352  infxpidmlem3OLD 9353  infxpidmlem8OLD 9358  infmap2 9380  dvdsabsb 9399  0dvds 9400  dvdsle 9422  dvdsleabs 9423  alzdvds 9424  divalglem10 9435  gcdval 9445  gcdcllem1 9448  gcdcllem2 9449  gcddvds 9452  isprm 9499  isprm2lem 9504  dvdsprm 9509  exprmfct 9517  maxprmfct 9519  prmexpb 9521  unbenlem 9522  infpnlem2 9525  infpn2 9527  1arithlem5 9534  1arithlem6 9535  1arithlem16 9545  1arithprmb 9552  poslem 9699  posasymb 9701  pleval2 9710  plttr 9715  pltletr 9716  lubprop 9724  lubid 9726  glbprop 9729  glble 9730  joinlem 9734  joinle 9737  meetval2 9740  meetlem 9741  lubl 9829  lubun 9832  qdensere 10043  metxp 10127  blfval2 10129  blval 10130  blrn2 10135  blelrn 10141  blin 10145  blss 10146  ssblex 10149  opnin 10162  blnei 10172  metcnp 10181  metcnpi 10184  metcnpi2 10185  metcnpi3 10186  metcnpi4 10187  metcni 10188  metcni2 10189  tgioolem 10208  lmcvg 10226  iscau3 10232  iscau4 10234  caun0 10239  lmuni 10245  lmle 10254  metelcls 10259  metelclsOLD 10260  metcnp4 10265  metcnp4OLD 10266  metcn4i 10268  xpcn 10272  lmcau 10292  bcthlem2 10296  bcthlem4 10298  bcthlem12 10306  bcthlem14 10308  bcthlem15 10309  bcthlem18 10312  bcthlem32 10326  gxval 10402  gapm 10483  vacnlem3 10690  nmcnilem 10697  va1cnlem 10705  sm1cnilem 10707  nmobndi 10798  blocni 10828  ubthlem1 10895  ubthlem14 10910  minveclem10 10924  minveclem27 10941  htthlem7 11000  spwmo 11026  spwpr4 11033  spwpr4OLD 11034  spwpr4aOLD 11035  pilem2 11048  pilem3 11049  pilem4 11050  sinhalfpilem 11055  efifolem5 11107  efif1lem5 11115  logltb 11157  dirtr 11352  tosdir 11354  axhcompl 11496  norm3lemt 11646  hcau2 11682  chlimi 11729  hlimcauii 11731  hlimcaui 11732  hlimuniii 11733  hlimunii 11734  hlimreui 11735  hlimeui 11736  occllem6 11803  occllem8 11805  projlem1 11811  projlem7 11817  projlem8 11818  projlem15 11825  projlem20 11830  projlem29 11839  cmbr3 12174  cmcm 12180  cmcm3 12181  lecm 12183  cnopc 12464  cnfnc 12481  0cnop 12530  0cnfn 12531  idcnop 12532  nmopun 12566  nmcopexlem1 12578  nmcopexlem6 12583  lnopconi 12590  nmcfnexlem1 12607  nmcfnexlem6 12612  lnfnconi 12617  nlelchi 12621  branmfn 12665  opsqrlem1 12700  pjnmopi 12708  hmopidmchi 12712  pjnormssi 12729  stge1i 12799  strlem5 12816  hstrlem5 12824  mddmd2 12870  csmdsymi 12895  cvmd 12897  ela 12900  cvbr3i 12928  irredlem3 12953  irredlem4 12954  irred 12956  atmd 12960  mdsym 12973  mddmdin0i 12992  cdj1i 12994  cdj3i 13002  bnj112 13397  bnj1185 13896  bnj602 14232  bnj1228 14385  bnj1482 14480  nqereu 14532  nsmallnq 14580  ltbtwnnq 14581  ltrnq 14582  prcdnq 14588  gch-aclem1 14600  prmexpbOLD 14603  sindivcvglem7 14639  epelg 14704  frirrc 14706  dfpo2 14712  fundmpss 14714  funbreq 14724  predbrg 14787  poxpOLD 14849  frxpOLD 14851  poseq 14854  axdenselem4 14938  axdenselem5 14939  axdense 14943  nocvxminlem 14944  axfelem9 14954  axfelem14 14959  axfelem16 14961  axfelem18 14963  brtxp 14999  elfix 15011  elfuns 15021  srefwref 15344  infxpg 15395  infsdomnng 15396  puub2 15600  puub 15601  supdef 15604  ismnl2 15610  defge3 15613  inposet 15620  rngsubpos 15636  dffprod 15670  cntrsetlem 16052  domleqt 16073  lvsovso 16093  tarval 16283  tarvalg 16284  tarval1 16285  tarval1g 16286  tclinf 16312  trer 16446  elicc3 16447  ccid 16448  finminlem 16452  finsschain 16458  ordtypelem2OLD 16461  ordtypelem6OLD 16465  ordtypelem7OLD 16466  ordtypeOLD 16467  onsdomOLD 16470  omsubsucOLD 16471  omsubsuc2OLD 16472  omsubsdomlem1OLD 16473  elomsubsdOLD 16479  omsubinitOLD 16484  fneerdm 16583  topfneec 16586  fnessref 16588  refssfne 16589  fnemeet2 16614  fcluscomplem 16705  eltail 16720  filnetlem3 16727  xpengOLD 16776  erthdmg 16815  findcard2OLD 16830  fimaxOLD 16831  fisupgOLD 16833  indexfiOLD 16840  frinfm 16843  fisup2gOLD 16853  frfiOLD 16856  frminexOLD 16858  add20 16862  fdc1 16898  nninfnub 16904  fsumltisumi 16908  fsumleisumi 16911  geomcau 16934  caushft 16936  metdcn 16938  oprpiece1res2 16966  haustlmu 16991  lmtlm 16993  txmet 17010  ismtyhmeolem 17035  heiborlem16 17055  heiborlem36 17075  bfplem8 17090  bfp 17094  recms 17095  rrncms 17104  phtpcdm 17146  ertr2 17342  erreft 17344  xrltneNEW 17519  lubunNEW 17826  oposlem 17840  glb0 17849  omllaw 17899  cvrval 17923  cvrnbtwn 17925  cvrnbtwn2 17928  cvrnbtwn3 17929  cvrcon3b 17930  cvrnbtwn4 17932  cvrcmp 17936  isat 17939  atnltOLD 17955  atnlt 17972  atlex 17975  cvlexch1 17988  cvlexchb1 17990  cvlatexch1 17996  glbcon 18035  2llnne2 18068  cvratlem 18081  cvrat4 18104  ps-1 18138  3at 18151  islln 18206  llncmp 18223  llnnlt 18224  islpln 18233  islpln5 18238  lvolex3 18241  lplncmp 18266  lplnexlln 18268  lplnnlt 18269  islvol 18277  lvoli3 18281  islvol5 18283  lvolcmp 18321  lvolnlt 18322  dalem-cly 18375  dalem44 18420  pmapval 18461  pmapglbx 18473  lncvrelat 18485  lncmp 18487  cdlemblem 18497  llnexchb2 18573  lautle 18713  lautleOLD 18714  lautcvr 18726  ldilset 18743  ltrnset 18752  trlset 18792  cdlemc4 18861  cdleme11d 18929  cdleme20k 18987  cdleme21ct 18997  cdleme22b 19009

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158  df-cleq 2163  df-clel 2166  df-v 2571  df-un 2864  df-sn 3274  df-pr 3275  df-op 3278  df-br 3540

Copyright terms: Public domain