Theorem breq2 2591

Description: Equality theorem for binary relation.

Assertion

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

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 2457	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	eleq1d 1516	. 2 |- (A = B -> (<.C, A>. e. R <-> <.C, B>. e. R))
3		df-br 2588	. 2 |- (CRA <-> <.C, A>. e. R)
4		df-br 2588	. 2 |- (CRB <-> <.C, B>. e. R)
5	2, 3, 4	3bitr4g 553	1 |- (A = B -> (CRA <-> CRB))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 1099   e. wcel 1105  <.cop 2382   class class class wbr 2587

This theorem is referenced by:  breq12 2592  breq2i 2595  breq2d 2598  pocl 2808  solin 2821  sotric 2824  sotrieq 2825  so 2828  dffr2 2882  frirr 2887  fr2nr 2888  fr3nr 2889  dfwe2 2898  wereu 2908  vtoclr 3173  vtoclrbr 3174  vtoclibr 3175  opelco 3245  opelcog 3247  opelcnvg 3253  resieq 3327  elimag 3358  eliniseg 3380  dffun3 3468  dffunmof 3471  fun11 3502  fv3 3672  tz6.12c 3679  tz6.12i 3680  funbrfv 3689  fnbrfvb 3692  funbrfvbg 3696  funfv2f 3711  dff2 3756  isorel 3833  isocnv 3835  isotr 3836  isotrALT 3837  isowe 3842  f1oiso 3843  f1oweALT 3845  caoprord 3996  ertr 4212  erref 4213  elec 4217  ecopoprsym 4248  ecopoprtrn 4249  th3qlem2 4253  domeng 4316  eqeng 4327  ensymg 4346  snfi 4367  xpdom1g 4378  sbth 4391  nneneq 4444  php2 4446  php3 4447  onfin 4451  ominf 4460  omsdomnn 4461  pssnn 4465  ssnn 4466  ssfi 4467  unfi 4480  unifi 4484  fiint 4486  abfii4 4490  fodomfi 4492  pwfi 4497  supmo 4502  supub 4506  suplub 4507  suppr 4514  supsnALT 4516  hta 4652  aceq3lem 4656  numth2 4709  zorn2lem2 4713  zorn2lem7 4718  zorn2 4720  fodomg 4723  brdom7disj 4728  brdom6disj 4729  unidomg 4733  oncardval 4743  cardval 4750  carden 4755  unxpdom 4767  sucxpdom 4769  cardlim 4774  cardmin 4783  alephnbtwn 4791  alephordlem1 4795  cardaleph 4808  alephval2 4825  dominf 4827  ltpiord 4938  indpi 4957  ltsopq 4998  ltapq 4999  ltmpq 5000  ltexpq 5003  nsmallpq 5006  ltbtwnpq 5007  ltrpq 5008  prcdpq 5020  genpcd 5032  genpnmax 5033  prlem934b 5061  ltaddpr2 5064  ltexprlem4 5068  reclem3pr 5081  supexpr 5086  ltsosr 5126  ltasr 5132  recexsrlem 5135  mulgt0sr 5137  map2psrpr 5143  suppsrlem 5144  suppsr 5145  suppsr2 5146  suppsr3 5147  supsrlem5 5152  supsrlem6 5153  supre 5183  ltsor 5184  pre-axltadd 5212  pre-axmulgt0 5213  ltletrt 5448  letrt 5449  pnfnemnf 5460  mnfltxrt 5469  xrltnsymt 5474  xrlttrit 5476  xrlttrt 5477  xrltletrt 5487  xrletrt 5488  ngtmnftt 5491  eqlet 5495  gt0ne0t 5543  ltadd1t 5548  leadd1t 5550  ltsubaddt 5552  lesubaddt 5554  lt2addt 5568  le2addt 5569  addgt0t 5571  addgegt0t 5572  addge0t 5574  ltnegt 5579  lenegt 5581  lesub0t 5602  mulge0t 5603  elimgt0 5716  elimge0 5717  prodgt0t 5733  prodge0t 5735  ltmul1t 5737  ltdiv1t 5756  ltmuldivt 5768  ltrec 5778  ltrect 5783  lerect 5784  lt2msqt 5785  le2msqt 5802  posex 5807  xrltmint 5813  lemint 5820  squeeze0 5823  nn2get 5841  nnge1t 5842  nnleltp1t 5852  nnsub 5854  nnsubt 5855  halfpost 5934  nominpos 5941  lbreu 5943  lble 5945  lbinfm 5946  sup2 5949  infm3 5952  infmsup 5966  infmrcl 5967  nnunb 5968  xrsupexmnf 5972  xrsupsslem 5974  xrinfmsslem 5975  xrub 5978  supxr 5979  supxrre 5981  supxrpnf 5986  supxrunb1 5987  supxrunb2 5988  lt0nnn0 6014  nn0ltp1let 6025  elnnz1 6053  nn0subt 6059  zltp1let 6079  z2get 6086  peano2uz2 6100  dfuz 6101  uzind 6104  uzind3 6106  uzindOLD 6107  uzind3OLD 6108  uzwo4OLD 6109  uzwo5OLD 6110  uzwo3lem2 6116  uzwo3 6117  zmin 6118  zmax 6119  zbtwnre 6120  rebtwnz 6121  flvalt 6124  flval2t 6132  flval3t 6133  qbtwnre 6167  qbtwnxr 6168  elrp 6171  monoord 6182  om2uzuz 6185  om2uzran 6188  uzrdgini 6191  uzrdginip1 6193  ioovalt 6254  iocvalt 6263  icovalt 6264  iccvalt 6265  elioo1t 6266  elioo2t 6267  elioc1t 6270  elico1t 6271  elicc1t 6272  iccsupr 6282  repos 6283  icoun 6297  snunioo 6299  eluz1t 6303  uzind4 6333  uzwo 6338  uzwoOLD 6339  nnwof 6342  fzvalt 6352  elfz1t 6353  fsequb 6406  seqzvalt 6423  seqz1 6430  sq11t 6511  sqrval 6552  sqr0 6553  sqrlem4 6557  sqrlem6 6559  sqrlem12 6565  sqrlem13 6566  sqrlem20 6573  sqrlem21 6574  sqrlem22 6575  sqrlem24 6577  sqrgt0i 6578  sqrlem26 6579  sqrclt 6591  sqrgt0t 6592  sqrge0t 6593  sqrlet 6594  sqr00t 6595  sqrsqt 6603  sqsqrt 6604  sqr2irrlem1 6605  sqr2irrlem2 6606  sqr2irr 6610  absidt 6748  absltt 6768  abslttOLD 6769  abslet 6770  abs3lemt 6795  seq1bnd 6798  cau3i 6802  cau3ir 6803  cvg2 6810  caubnd 6814  facdivt 6830  facwordit 6832  bcvalt 6846  bcpasc2t 6857  bccl2t 6860  dffsum 6887  clm4le 6970  clmi1 6975  climuni 6987  climeu 6988  2climnn 6990  2climnn0 6991  climshft 6992  iserzshft2 6995  climrecl 6998  climge0 7000  climaddlem3 7003  climmullem8 7014  iserzext 7022  climcmplem 7024  iserzex 7033  climubi 7040  climsup 7042  climcau 7043  caucvglem2 7045  caucvglem6 7049  caucvg 7050  caucvg2 7052  caucvg3lem 7053  caucvg3t 7055  serzf0 7056  ser1f0 7057  ser1cmp2 7064  cvgcmp2lem 7067  cvgcmpub 7072  cvgcmp3ce 7074  cvgcmp3cetlem1 7075  cvgcmp3cetlem2 7076  isumclimtf 7082  isumsplit 7102  infcvglem1 7107  expcnvlem3 7115  expcnvlem5 7117  geoisum1c 7131  cvgratlem1ALT 7133  cvgratlem1 7136  cvgratlem4 7139  elcncf1d 7156  ivthlem2 7168  ivthlem4OLD 7179  efseq1ex 7199  efseq0ex 7204  efaddlem24 7254  eflegeot 7307  efm1legeot 7309  efcnlem4 7313  efcn 7314  reeff1olem2 7316  reeff1olem2OLD 7318  reefiso 7321  acdc3 7380  acdc2 7383  acdc5 7386  acdc 7388  unbenlem 7398  infpnlem2 7401  infpn2 7403  ruclem4 7407  ruclem33 7436  ruclem35 7438  ruclem36 7439  infxpidmlem2 7447  infxpidmlem3 7448  infxpidmlem8 7453  infmap2 7474  qdensere 7639  metxp 7722  blfval2 7724  blval 7725  blrn2 7730  blelrn 7736  blin 7740  blss 7741  ssblex 7744  opnin 7757  blnei 7766  metcnp 7774  metcnpi 7777  metcnpi2 7778  metcnpi3 7779  metcnpi4 7780  metcni 7781  metcni2 7782  tgioolem 7801  lmcvg 7818  iscau3 7824  caun0 7828  lmuni 7834  lmle 7843  metelcls 7848  metcnp4 7852  metcn4i 7854  xpcn 7858  lmcau 7878  bcthlem2 7882  bcthlem4 7884  bcthlem12 7892  bcthlem14 7894  bcthlem15 7895  bcthlem18 7898  bcthlem32 7912  nmcnilem 8209  va1cnlem 8214  sm1cnilem 8216  nmobndi 8305  blocni 8331  ubthlem1 8395  ubthlem14 8408  minveclem10 8420  minveclem27 8437  htthlem7 8490  pilem2 8504  pilem3 8505  pilem4 8506  sinhalfpilem 8511  efifolem5 8554  efif1lem5 8562  logltbt 8611  logltbtOLD 8628  infi 8798  norm3lemt 9168  hcau2 9205  chlim 9255  hlimcaui 9257  hlimcau 9258  hlimunii 9259  hlimuni 9260  hlimreu 9261  hlimeu 9262  occllem6 9308  occllem8 9310  projlem1 9316  projlem7 9322  projlem8 9323  projlem15 9330  projlem20 9335  projlem29 9344  cmbr3t 9682  cmcmt 9688  cmcm3t 9689  lecmt 9691  cnopct 9967  cnfnct 9984  0cnop 10033  0cnfn 10034  idcnop 10035  nmopunt 10068  nmcopexlem1 10080  nmcopexlem6 10085  lnopcon 10092  nmcfnexlem1 10109  nmcfnexlem6 10114  lnfncon 10119  nlelch 10123  branmfnt 10165  pjnmop 10200  hmopidmch 10204  pjnormss 10221  stge1 10289  strlem5 10306  hstrlem5 10314  mddmd 10358  csmdsym 10383  cvmdt 10385  elat 10388  cvbr3 10416  irredlem3 10441  irredlem4 10442  irredt 10444  atmd 10448  mdsymt 10461  mddmdin0 10477  cdj1 10479  cdj3 10487

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-un 2021  df-sn 2383  df-pr 2384  df-op 2387  df-br 2588

Copyright terms: Public domain