Theorem breq2 2629

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 2493	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	eleq1d 1543	. 2 |- (A = B -> (<.C, A>. e. R <-> <.C, B>. e. R))
3		df-br 2626	. 2 |- (CRA <-> <.C, A>. e. R)
4		df-br 2626	. 2 |- (CRB <-> <.C, B>. e. R)
5	2, 3, 4	3bitr4g 557	1 |- (A = B -> (CRA <-> CRB))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 958   e. wcel 960  <.cop 2416   class class class wbr 2625

This theorem is referenced by:  breq12 2630  breq2i 2633  breq2d 2636  pocl 2851  solin 2864  sotric 2867  sotrieq 2868  so 2871  dffr2 2926  frirr 2931  fr2nr 2932  fr3nr 2933  dfwe2 2942  wereu 2952  vtoclr 3218  vtoclrbr 3219  vtoclibr 3220  ididg 3285  opelco 3295  opelcog 3297  opelcnvg 3303  resieq 3383  elimag 3414  eliniseg 3436  asymref2 3447  dffun3 3534  dffunmof 3537  fun11 3569  fv3 3740  tz6.12c 3747  tz6.12i 3748  funbrfv 3757  fnbrfvb 3760  funbrfvbg 3764  funfv2f 3779  dff2 3824  isorel 3901  isocnv 3903  isotr 3904  isotrALT 3905  isowe 3910  f1oiso 3911  f1oweALT 3913  caoprord 4063  ertr 4281  erref 4282  elec 4286  ecopoprsym 4317  ecopoprtrn 4318  th3qlem2 4322  domeng 4387  eqeng 4399  ensymg 4418  snfi 4439  snfiOLD 4440  xpdom1g 4451  sbth 4464  nneneq 4519  php2 4521  php3OLD 4523  onfin 4527  ominfOLD 4539  omsdomnn 4540  pssnn 4546  ssnnfi 4547  ssnnfiOLD 4548  ssfiOLD 4550  unfi 4565  unfiOLD 4566  unifi 4572  unifiOLD 4574  fiint 4576  fiintOLD 4577  fodomfi 4582  fodomfiOLD 4583  pwfiOLD 4587  supmo 4592  supub 4596  suplub 4597  supmaxlem 4604  suppr 4606  supsnALT 4608  hta 4745  aceq3lem 4749  numth2 4802  zorn2lem2 4806  zorn2lem7 4811  zorn2 4813  fodomg 4816  brdom7disj 4821  brdom6disj 4822  unidomg 4826  oncardval 4836  cardval 4843  carden 4848  unxpdom 4862  sucxpdom 4864  cardlim 4869  cardmin 4878  alephnbtwn 4886  alephordlem1 4890  cardaleph 4903  alephval2 4920  dominf 4922  dominfOLD 4923  ltpiord 5034  indpi 5053  ltsopq 5094  ltapq 5095  ltmpq 5096  ltexpq 5099  nsmallpq 5102  ltbtwnpq 5103  ltrpq 5104  prcdpq 5116  genpcd 5128  genpnmax 5129  prlem934b 5157  ltaddpr2 5160  ltexprlem4 5164  reclem3pr 5177  supexpr 5182  ltsosr 5222  ltasr 5228  recexsrlem 5231  mulgt0sr 5233  map2psrpr 5239  suppsrlem 5240  suppsr 5241  suppsr2 5242  suppsr3 5243  supsrlem5 5248  supsrlem6 5249  supre 5279  ltsor 5280  pre-axltadd 5308  pre-axmulgt0 5309  ltletrt 5543  letrt 5544  pnfnemnf 5555  mnfltxrt 5564  xrltnsymt 5569  xrlttrit 5571  xrlttrt 5572  xrltletrt 5582  xrletrt 5583  ngtmnftt 5586  eqlet 5590  gt0ne0t 5637  ltadd1t 5642  leadd1t 5644  ltsubaddt 5646  lesubaddt 5648  lt2addt 5662  le2addt 5663  addgt0t 5666  addgegt0t 5667  addge0t 5669  ltnegt 5674  lenegt 5676  lesub0t 5697  mulge0t 5698  elimgt0 5818  elimge0 5819  prodgt0t 5835  prodge0t 5837  ltmul1t 5839  ltdiv1t 5858  ltdiv1tOLD 5859  ltmuldivt 5872  ltmuldivtOLD 5873  ltrec 5888  ltrect 5893  lerect 5894  lt2msqt 5895  le2msqt 5912  posex 5917  xrltmint 5923  lemint 5930  squeeze0 5933  nn2get 5951  nnge1t 5952  nnleltp1t 5963  nnsub 5965  nnsubt 5966  halfpost 6045  nominpos 6052  lbreu 6054  lble 6056  lbinfm 6057  sup2 6060  infm3 6063  infmsup 6077  infmrcl 6078  nnunb 6079  xrsupexmnf 6083  xrsupsslem 6085  xrinfmsslem 6086  xrub 6089  supxr 6090  supxrre 6092  supxrpnf 6097  supxrunb1 6098  supxrunb2 6099  lt0nnn0 6125  nn0ltp1let 6136  elnnz1 6164  nn0subt 6170  zltp1let 6190  z2get 6197  peano2uz2 6210  dfuz 6211  uzind 6214  uzind3 6216  uzindOLD 6217  uzind3OLD 6218  uzwo4OLD 6219  uzwo5OLD 6220  uzwo3lem2 6226  uzwo3 6227  zmin 6228  zmax 6229  zbtwnre 6230  rebtwnz 6231  flvalt 6234  flval2t 6247  flval3t 6248  qbtwnre 6286  qbtwnxr 6287  elrp 6290  monoord 6302  om2uzuz 6305  om2uzran 6308  uzrdgini 6311  uzrdginip1 6313  ioovalt 6374  iocvalt 6383  icovalt 6384  iccvalt 6385  elioo1t 6386  elioo2t 6387  elioc1t 6389  elico1t 6390  elicc1t 6391  iccsupr 6406  repos 6407  icoun 6421  snunioo 6423  eluz1t 6428  uzind4 6458  uzwo 6463  uzwoOLD 6464  nnwof 6467  fzvalt 6477  elfz1t 6478  fsequb 6531  seqzvalt 6548  seqz1 6555  sq11t 6637  sqrval 6679  sqr0 6680  sqrlem4 6684  sqrlem6 6686  sqrlem12 6692  sqrlem13 6693  sqrlem20 6700  sqrlem21 6701  sqrlem22 6702  sqrlem24 6704  sqrgt0i 6705  sqrlem26 6706  sqrclt 6718  sqrgt0t 6719  sqrge0t 6720  sqrlet 6721  sqr00t 6722  sqrsqt 6730  sqsqrt 6731  sqr2irrlem1 6732  sqr2irrlem2 6733  sqr2irr 6737  absidt 6869  absltt 6887  abslet 6888  abs3lemt 6914  seq1bnd 6917  cau3i 6921  cau3ir 6922  cvg2 6929  caubnd 6933  facdivt 6949  facwordit 6951  bcvalt 6965  bcpasc2t 6975  bccl2t 6978  dffsum 7005  clm4le 7088  clmi1 7093  climuni 7106  climeu 7107  2climnn 7109  2climnn0 7110  climshft 7111  iserzshft2 7114  climrecl 7117  climge0 7119  climaddlem3 7123  climmullem8 7134  iserzext 7142  climcmplem 7144  iserzex 7153  climubi 7160  climsup 7162  climcau 7163  caucvglem2 7165  caucvglem6 7169  caucvg 7170  caucvg2 7172  caucvg3lem 7173  caucvg3t 7175  serzf0 7176  ser1f0 7177  ser1cmp2 7184  cvgcmp2lem 7187  cvgcmpub 7192  cvgcmp3ce 7194  cvgcmp3cetlem1 7195  cvgcmp3cetlem2 7196  isumclimtf 7202  isumsplit 7223  infcvglem1 7228  expcnvlem3 7236  expcnvlem5 7238  geoisum1c 7252  cvgratlem1ALT 7254  cvgratlem1 7257  cvgratlem4 7260  elcncf1d 7277  ivthlem2 7289  efseq1ex 7313  efseq0ex 7318  efaddlem24 7368  eflegeot 7423  efm1legeot 7425  efcnlem4 7429  efcn 7430  reeff1olem2 7432  reefiso 7435  acdc3 7495  acdc2 7498  acdc5 7501  acdc 7503  unbenlem 7512  infpnlem2 7515  infpn2 7517  ruclem4 7521  ruclem33 7550  ruclem35 7552  ruclem36 7553  infxpidmlem2 7561  infxpidmlem3 7562  infxpidmlem8 7567  infmap2 7590  qdensere 7755  metxp 7838  blfval2 7840  blval 7841  blrn2 7846  blelrn 7852  blin 7856  blss 7857  ssblex 7860  opnin 7873  blnei 7883  metcnp 7891  metcnpi 7894  metcnpi2 7895  metcnpi3 7896  metcnpi4 7897  metcni 7898  metcni2 7899  tgioolem 7918  lmcvg 7936  iscau3 7942  iscau4 7944  caun0 7949  lmuni 7955  lmle 7964  metelcls 7969  metcnp4 7974  metcn4i 7976  xpcn 7980  lmcau 8000  bcthlem2 8004  bcthlem4 8006  bcthlem12 8014  bcthlem14 8016  bcthlem15 8017  bcthlem18 8020  bcthlem32 8034  nmcnilem 8340  va1cnlem 8348  sm1cnilem 8350  nmobndi 8441  blocni 8468  ubthlem1 8532  ubthlem14 8545  minveclem10 8557  minveclem27 8574  htthlem7 8629  spwmo 8659  spwpr4OLD 8665  spwpr4aOLD 8666  pilem2 8674  pilem3 8675  pilem4 8676  sinhalfpilem 8681  efifolem5 8728  efif1lem5 8736  logltbt 8778  axhcompl 8870  norm3lemt 9021  hcau2 9057  chlim 9106  hlimcaui 9108  hlimcau 9109  hlimunii 9110  hlimuni 9111  hlimreu 9112  hlimeu 9113  occllem6 9180  occllem8 9182  projlem1 9188  projlem7 9194  projlem8 9195  projlem15 9202  projlem20 9207  projlem29 9216  cmbr3t 9553  cmcmt 9559  cmcm3t 9560  lecmt 9562  cnopct 9839  cnfnct 9856  0cnop 9905  0cnfn 9906  idcnop 9907  nmopunt 9941  nmcopexlem1 9953  nmcopexlem6 9958  lnopcon 9965  nmcfnexlem1 9982  nmcfnexlem6 9987  lnfncon 9992  nlelch 9996  branmfnt 10040  pjnmop 10077  hmopidmch 10081  pjnormss 10098  stge1 10168  strlem5 10185  hstrlem5 10193  mddmd 10239  csmdsym 10264  cvmdt 10266  elat 10269  cvbr3 10297  irredlem3 10322  irredlem4 10323  irredt 10325  atmd 10329  mdsymt 10342  mddmdin0 10361  cdj1 10363  cdj3 10371  inposet 10485

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2054  df-sn 2417  df-pr 2418  df-op 2421  df-br 2626

Copyright terms: Public domain