Theorem breq2 2696

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 2553	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	eleq1d 1583	. 2 |- (A = B -> (<.C, A>. e. R <-> <.C, B>. e. R))
3		df-br 2693	. 2 |- (CRA <-> <.C, A>. e. R)
4		df-br 2693	. 2 |- (CRB <-> <.C, B>. e. R)
5	2, 3, 4	3bitr4g 558	1 |- (A = B -> (CRA <-> CRB))

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992   e. wcel 994  <.cop 2469   class class class wbr 2692

This theorem is referenced by:  breq12 2697  breq2i 2700  breq2d 2703  pocl 2922  posn 2928  solin 2936  sotric 2939  sotrieq 2940  so 2943  dffr2 2949  frirr 2954  fr2nr 2955  wereu 2972  fr3nr 3138  dfwe2 3140  vtoclr 3294  vtoclrbr 3295  vtoclibr 3296  ididg 3368  opelco 3378  opelco2g 3380  opelcnvg 3387  resieq 3463  elimag 3499  eliniseg 3521  asymref2 3532  dffun3 3632  dffun6f 3635  fun11 3667  fv3 3844  tz6.12c 3851  tz6.12i 3852  funbrfv 3861  fnbrfvb 3864  funbrfvbg 3868  funfv2f 3883  dff3 3931  isorel 4008  isocnv 4010  isotr 4011  isotrALT 4012  isowe 4017  f1oiso 4018  f1oweALT 4020  caoprord 4117  ertr 4414  erref 4415  elec 4419  ecopoprsym 4451  ecopoprtrn 4452  th3qlem2 4456  domeng 4521  eqeng 4533  ensymg 4552  snfi 4573  xpdom1g 4585  sbth 4602  nneneq 4659  php2 4661  onfin 4666  omsdomnn 4676  pssnn 4681  ssnnfi 4682  unfi 4697  unifi 4701  fiint 4703  fodomfi 4709  supmo 4719  supub 4723  suplub 4724  supmaxlem 4731  suppr 4733  supsnALT 4735  hta 4874  aceq3lem 4878  numth2 4931  zorn2lem2 4935  zorn2lem7 4940  zorn2 4942  fodomg 4945  brdom7disj 4950  brdom6disj 4951  unidomg 4955  oncardval 4965  cardval 4973  carden 4979  unxpdom 4994  sucxpdom 4996  cardlim 5001  cardmin 5010  alephnbtwn 5018  alephordlem1 5022  cardaleph 5035  alephval2 5052  dominf 5054  cdaeng 5076  ltpiord 5169  indpi 5188  ltsopq 5229  ltapq 5230  ltmpq 5231  ltexpq 5234  nsmallpq 5237  ltbtwnpq 5238  ltrpq 5239  prcdpq 5251  genpcd 5263  genpnmax 5264  prlem934b 5292  ltaddpr2 5295  ltexprlem4 5299  reclem3pr 5312  supexpr 5317  ltsosr 5357  ltasr 5363  recexsrlem 5366  mulgt0sr 5368  map2psrpr 5374  suppsrlem 5375  suppsr 5376  suppsr2 5377  suppsr3 5378  supsrlem5 5383  supsrlem6 5384  supre 5414  ltsor 5415  pre-axltadd 5443  pre-axmulgt0 5444  ltletr 5678  letr 5679  mnfltxr 5699  xrltnsym 5704  xrlttri 5706  xrlttr 5707  xrltletr 5717  xrletr 5718  ngtmnft 5721  eqle 5725  gt0ne0 5772  ltadd1 5777  leadd1 5779  ltsubadd 5781  lesubadd 5783  lt2add 5797  le2add 5798  addgt0 5801  addgegt0 5802  addge0 5804  ltneg 5809  leneg 5811  lesub0 5832  mulge0 5833  mulge0OLD 5834  elimgt0 5949  elimge0 5950  prodgt0 5966  prodge0 5968  ltmul1 5970  ltdiv1 5993  ltdiv1OLD 5994  ltmuldiv 6007  ltmuldivOLD 6008  ltreci 6024  ltrec 6029  lerec 6030  lt2msq 6031  le2msq 6048  posexi 6053  xrltmin 6059  lemin 6066  squeeze0 6069  nn2ge 6087  nnge1 6088  nnleltp1 6100  nnsubi 6102  nnsub 6103  halfpos 6182  nominpos 6189  elrp 6192  lbreu 6213  lble 6215  lbinfm 6216  sup2 6219  infm3 6222  infmsup 6236  infmrcl 6237  nnunb 6238  xrsupexmnf 6242  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxr 6249  supxrre 6251  supxrpnf 6256  supxrunb1 6257  supxrunb2 6258  lt0nnn0 6284  nn0ltp1le 6295  elnnz1 6323  nn0sub 6329  zltp1le 6349  z2ge 6359  peano2uz2 6372  dfuzi 6373  uzind 6376  uzind3 6378  uzindOLD 6379  uzind3OLD 6380  uzwo4OLD 6381  uzwo5OLD 6382  uzwo3lem2 6389  uzwo3 6390  zmin 6391  zmax 6392  zbtwnre 6393  rebtwnz 6394  qbtwnre 6418  qbtwnxr 6419  flval 6423  flval2 6437  flval3 6438  modid2 6472  monoord 6482  iooval 6492  iocval 6501  icoval 6502  iccval 6503  elioo1 6504  elioo2 6505  elioc1 6507  elico1 6508  elicc1 6509  iccsupr 6525  repos 6526  icoun 6540  snunioo 6542  eluz1 6547  uzind4 6577  uzwo 6582  uzwoOLD 6583  nnwof 6586  fzval 6597  elfz1 6598  fzsuc 6636  fsequb 6654  om2uzuzi 6660  om2uzrani 6663  uzrdginii 6667  uzrdginip1i 6669  seqzval 6735  seqz1 6742  sq11 6826  sqrval 6872  sqr0 6873  sqrlem4 6877  sqrlem6 6879  sqrlem12 6885  sqrlem13 6886  sqrlem20 6893  sqrlem21 6894  sqrlem22 6895  sqrlem24 6897  sqrgt0ii 6898  sqrlem26 6899  sqrcl 6911  sqrgt0 6912  sqrge0 6913  sqrle 6914  sqr00 6915  sqrsq 6923  sqsqr 6924  sqr2irrlem1 6925  sqr2irrlem2 6926  sqr2irr 6930  absid 7064  abslt 7083  absle 7084  abs3lem 7110  seq1bndi 7113  cau3ii 7117  cau3iri 7118  cvg2i 7125  caubndi 7129  facdiv 7145  facwordi 7147  bcval 7161  bcpasc2 7171  bccl2 7174  dffsum 7201  clm4lei 7284  clmi1i 7289  climuni 7302  climeu 7303  2climnn 7305  2climnn0 7306  climshfti 7307  iserzshft2i 7310  climrecl 7313  climge0 7315  climaddlem3 7319  climmullem8 7330  iserzex 7338  climcmplem 7340  iserzexi 7349  climubii 7356  climsupi 7358  climcaui 7359  caucvglem2 7361  caucvglem6 7365  caucvgi 7366  caucvg2i 7368  caucvg3lem 7369  caucvg3 7371  serzf0i 7372  ser1cmp2i 7380  cvgcmp2lem 7383  cvgcmpubi 7389  cvgcmp3cei 7391  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  isumclimtfi 7399  isumspliti 7420  infcvglem1 7425  expcnvlem3 7433  expcnvlem5 7435  geoisum1c 7450  cvgratlem1ALT 7452  cvgratlem1 7455  cvgratlem4 7458  elcncf1di 7475  ivthlem2 7487  efseq1ex 7511  efseq0ex 7516  efaddlem24 7566  eflegeo 7624  efm1legeo 7626  efcnlem4 7630  efcn 7631  reeff1olem2 7633  reefiso 7636  acdc3 7698  acdc2 7702  acdc5 7705  acdc 7707  unbenlem 7716  infpnlem2 7719  infpn2 7721  ruclem4 7725  ruclem33 7754  ruclem35 7756  ruclem36 7757  infxpidmlem2 7765  infxpidmlem3 7766  infxpidmlem8 7771  infmap2 7793  qdensere 7961  metxp 8044  blfval2 8046  blval 8047  blrn2 8052  blelrn 8058  blin 8062  blss 8063  ssblex 8066  opnin 8079  blnei 8089  metcnp 8098  metcnpi 8101  metcnpi2 8102  metcnpi3 8103  metcnpi4 8104  metcni 8105  metcni2 8106  tgioolem 8125  lmcvg 8143  iscau3 8149  iscau4 8151  caun0 8156  lmuni 8162  lmle 8171  metelcls 8176  metcnp4 8181  metcn4i 8183  xpcn 8187  lmcau 8207  bcthlem2 8211  bcthlem4 8213  bcthlem12 8221  bcthlem14 8223  bcthlem15 8224  bcthlem18 8227  bcthlem32 8241  gxval 8314  vacnlem3 8584  nmcnilem 8591  va1cnlem 8599  sm1cnilem 8601  nmobndi 8692  blocni 8720  ubthlem1 8787  ubthlem14 8802  minveclem10 8814  minveclem27 8831  htthlem7 8888  spwmo 8918  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  pilem2 8939  pilem3 8940  pilem4 8941  sinhalfpilem 8946  efifolem5 8998  efif1lem5 9006  logltb 9048  axhcompl 9143  norm3lemt 9295  hcau2 9331  chlimi 9380  hlimcauii 9382  hlimcaui 9383  hlimuniii 9384  hlimunii 9385  hlimreui 9386  hlimeui 9387  occllem6 9454  occllem8 9456  projlem1 9462  projlem7 9468  projlem8 9469  projlem15 9476  projlem20 9481  projlem29 9490  cmbr3 9827  cmcm 9833  cmcm3 9834  lecm 9836  cnopc 10117  cnfnc 10134  0cnop 10182  0cnfn 10183  idcnop 10184  nmopun 10218  nmcopexlem1 10230  nmcopexlem6 10235  lnopconi 10242  nmcfnexlem1 10259  nmcfnexlem6 10264  lnfnconi 10269  nlelchi 10273  branmfn 10317  branmfnOLD 10318  pjnmopi 10355  hmopidmchi 10359  pjnormssi 10376  stge1i 10446  strlem5 10463  hstrlem5 10471  mddmd2 10517  csmdsymi 10542  cvmd 10544  ela 10547  cvbr3i 10575  irredlem3 10601  irredlem4 10602  irred 10604  atmd 10608  mdsym 10621  mddmdin0i 10640  cdj1i 10642  cdj3i 10650  domleqt 10792  inposet 10868  trer 11409  elicc3 11410  ccid 11412  finminlem 11418  finsschain 11425  ordtypelem2 11428  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  onsdom 11437  omsubsuc 11438  omsubsuc2 11439  omsubsdomlem1 11440  elomsubsd 11446  omsubinit 11451  fneerdm 11559  topfneec 11562  fnessref 11564  refssfne 11565  fnemeet2 11590  fcluscomplem 11732  dirtr 11753  tosdir 11755  eltail 11758  filnetlem3 11765  gapm 11784  erthdmg 11824  dif1en 11833  ficard 11834  dif1card 11835  fimax 11837  fisupg 11839  indexf 11847  frinfm 11850  add20 11858  nninfnub 11882  fsumltisumi 11886  fsumleisumi 11889  metsstop 11909  geomcau 11914  caushft 11916  metdcn 11918  haustlmu 11967  lmtlm 11969  ismtyhmeolem 12006  heiborlem16 12026  heiborlem36 12046  bfplem8 12061  bfp 12065  recms 12066  rrncms 12075  phtpcdm 12103

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-sn 2470  df-pr 2471  df-op 2474  df-br 2693

Copyright terms: Public domain