Theorem breq2 2628

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 2492	. . 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 2625	. 2 |- (CRA <-> <.C, A>. e. R)
4		df-br 2625	. 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 2415   class class class wbr 2624

This theorem is referenced by:  breq12 2629  breq2i 2632  breq2d 2635  pocl 2850  solin 2863  sotric 2866  sotrieq 2867  so 2870  dffr2 2925  frirr 2930  fr2nr 2931  fr3nr 2932  dfwe2 2941  wereu 2951  vtoclr 3217  vtoclrbr 3218  vtoclibr 3219  ididg 3284  opelco 3294  opelcog 3296  opelcnvg 3302  resieq 3382  elimag 3413  eliniseg 3435  asymref2 3446  dffun3 3533  dffunmof 3536  fun11 3568  fv3 3739  tz6.12c 3746  tz6.12i 3747  funbrfv 3756  fnbrfvb 3759  funbrfvbg 3763  funfv2f 3778  dff2 3823  isorel 3900  isocnv 3902  isotr 3903  isotrALT 3904  isowe 3909  f1oiso 3910  f1oweALT 3912  caoprord 4062  ertr 4280  erref 4281  elec 4285  ecopoprsym 4316  ecopoprtrn 4317  th3qlem2 4321  domeng 4386  eqeng 4398  ensymg 4417  snfi 4438  snfiOLD 4439  xpdom1g 4450  sbth 4463  nneneq 4518  php2 4520  php3OLD 4522  ominfOLD 4537  omsdomnn 4538  pssnn 4544  ssnnfi 4545  ssnnfiOLD 4546  ssfiOLD 4548  unfi 4563  unfiOLD 4564  unifiOLD 4570  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  pwfiOLD 4580  supmo 4585  supub 4589  suplub 4590  supmaxlem 4597  suppr 4599  supsnALT 4601  hta 4738  aceq3lem 4742  numth2 4795  zorn2lem2 4799  zorn2lem7 4804  zorn2 4806  fodomg 4809  brdom7disj 4814  brdom6disj 4815  unidomg 4819  oncardval 4829  cardval 4836  carden 4841  unxpdom 4855  sucxpdom 4857  cardlim 4862  cardmin 4871  alephnbtwn 4879  alephordlem1 4883  cardaleph 4896  alephval2 4913  dominf 4915  dominfOLD 4916  ltpiord 5027  indpi 5046  ltsopq 5087  ltapq 5088  ltmpq 5089  ltexpq 5092  nsmallpq 5095  ltbtwnpq 5096  ltrpq 5097  prcdpq 5109  genpcd 5121  genpnmax 5122  prlem934b 5150  ltaddpr2 5153  ltexprlem4 5157  reclem3pr 5170  supexpr 5175  ltsosr 5215  ltasr 5221  recexsrlem 5224  mulgt0sr 5226  map2psrpr 5232  suppsrlem 5233  suppsr 5234  suppsr2 5235  suppsr3 5236  supsrlem5 5241  supsrlem6 5242  supre 5272  ltsor 5273  pre-axltadd 5301  pre-axmulgt0 5302  ltletrt 5536  letrt 5537  pnfnemnf 5548  mnfltxrt 5557  xrltnsymt 5562  xrlttrit 5564  xrlttrt 5565  xrltletrt 5575  xrletrt 5576  ngtmnftt 5579  eqlet 5583  gt0ne0t 5630  ltadd1t 5635  leadd1t 5637  ltsubaddt 5639  lesubaddt 5641  lt2addt 5655  le2addt 5656  addgt0t 5659  addgegt0t 5660  addge0t 5662  ltnegt 5667  lenegt 5669  lesub0t 5690  mulge0t 5691  elimgt0 5811  elimge0 5812  prodgt0t 5828  prodge0t 5830  ltmul1t 5832  ltdiv1t 5851  ltdiv1tOLD 5852  ltmuldivt 5865  ltmuldivtOLD 5866  ltrec 5881  ltrect 5886  lerect 5887  lt2msqt 5888  le2msqt 5905  posex 5910  xrltmint 5916  lemint 5923  squeeze0 5926  nn2get 5944  nnge1t 5945  nnleltp1t 5956  nnsub 5958  nnsubt 5959  halfpost 6038  nominpos 6045  lbreu 6047  lble 6049  lbinfm 6050  sup2 6053  infm3 6056  infmsup 6070  infmrcl 6071  nnunb 6072  xrsupexmnf 6076  xrsupsslem 6078  xrinfmsslem 6079  xrub 6082  supxr 6083  supxrre 6085  supxrpnf 6090  supxrunb1 6091  supxrunb2 6092  lt0nnn0 6118  nn0ltp1let 6129  elnnz1 6157  nn0subt 6163  zltp1let 6183  z2get 6190  peano2uz2 6203  dfuz 6204  uzind 6207  uzind3 6209  uzindOLD 6210  uzind3OLD 6211  uzwo4OLD 6212  uzwo5OLD 6213  uzwo3lem2 6219  uzwo3 6220  zmin 6221  zmax 6222  zbtwnre 6223  rebtwnz 6224  flvalt 6227  flval2t 6240  flval3t 6241  qbtwnre 6279  qbtwnxr 6280  elrp 6283  monoord 6295  om2uzuz 6298  om2uzran 6301  uzrdgini 6304  uzrdginip1 6306  ioovalt 6367  iocvalt 6376  icovalt 6377  iccvalt 6378  elioo1t 6379  elioo2t 6380  elioc1t 6382  elico1t 6383  elicc1t 6384  iccsupr 6399  repos 6400  icoun 6414  snunioo 6416  eluz1t 6421  uzind4 6451  uzwo 6456  uzwoOLD 6457  nnwof 6460  fzvalt 6470  elfz1t 6471  fsequb 6524  seqzvalt 6541  seqz1 6548  sq11t 6630  sqrval 6672  sqr0 6673  sqrlem4 6677  sqrlem6 6679  sqrlem12 6685  sqrlem13 6686  sqrlem20 6693  sqrlem21 6694  sqrlem22 6695  sqrlem24 6697  sqrgt0i 6698  sqrlem26 6699  sqrclt 6711  sqrgt0t 6712  sqrge0t 6713  sqrlet 6714  sqr00t 6715  sqrsqt 6723  sqsqrt 6724  sqr2irrlem1 6725  sqr2irrlem2 6726  sqr2irr 6730  absidt 6862  absltt 6880  abslet 6881  abs3lemt 6907  seq1bnd 6910  cau3i 6914  cau3ir 6915  cvg2 6922  caubnd 6926  facdivt 6942  facwordit 6944  bcvalt 6958  bcpasc2t 6968  bccl2t 6971  dffsum 6998  clm4le 7081  clmi1 7086  climuni 7099  climeu 7100  2climnn 7102  2climnn0 7103  climshft 7104  iserzshft2 7107  climrecl 7110  climge0 7112  climaddlem3 7116  climmullem8 7127  iserzext 7135  climcmplem 7137  iserzex 7146  climubi 7153  climsup 7155  climcau 7156  caucvglem2 7158  caucvglem6 7162  caucvg 7163  caucvg2 7165  caucvg3lem 7166  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1cmp2 7177  cvgcmp2lem 7180  cvgcmpub 7185  cvgcmp3ce 7187  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  isumclimtf 7195  isumsplit 7216  infcvglem1 7221  expcnvlem3 7229  expcnvlem5 7231  geoisum1c 7245  cvgratlem1ALT 7247  cvgratlem1 7250  cvgratlem4 7253  elcncf1d 7270  ivthlem2 7282  efseq1ex 7306  efseq0ex 7311  efaddlem24 7361  eflegeot 7416  efm1legeot 7418  efcnlem4 7422  efcn 7423  reeff1olem2 7425  reefiso 7428  acdc3 7488  acdc2 7491  acdc5 7494  acdc 7496  unbenlem 7505  infpnlem2 7508  infpn2 7510  ruclem4 7514  ruclem33 7543  ruclem35 7545  ruclem36 7546  infxpidmlem2 7554  infxpidmlem3 7555  infxpidmlem8 7560  infmap2 7583  qdensere 7748  metxp 7831  blfval2 7833  blval 7834  blrn2 7839  blelrn 7845  blin 7849  blss 7850  ssblex 7853  opnin 7866  blnei 7876  metcnp 7884  metcnpi 7887  metcnpi2 7888  metcnpi3 7889  metcnpi4 7890  metcni 7891  metcni2 7892  tgioolem 7911  lmcvg 7929  iscau3 7935  iscau4 7937  caun0 7942  lmuni 7948  lmle 7957  metelcls 7962  metcnp4 7967  metcn4i 7969  xpcn 7973  lmcau 7993  bcthlem2 7997  bcthlem4 7999  bcthlem12 8007  bcthlem14 8009  bcthlem15 8010  bcthlem18 8013  bcthlem32 8027  nmcnilem 8333  va1cnlem 8341  sm1cnilem 8343  nmobndi 8434  blocni 8461  ubthlem1 8525  ubthlem14 8538  minveclem10 8550  minveclem27 8567  htthlem7 8622  spwmo 8652  spwpr4OLD 8658  spwpr4aOLD 8659  pilem2 8667  pilem3 8668  pilem4 8669  sinhalfpilem 8674  efifolem5 8721  efif1lem5 8729  logltbt 8771  axhcompl 8863  norm3lemt 9014  hcau2 9050  chlim 9099  hlimcaui 9101  hlimcau 9102  hlimunii 9103  hlimuni 9104  hlimreu 9105  hlimeu 9106  occllem6 9173  occllem8 9175  projlem1 9181  projlem7 9187  projlem8 9188  projlem15 9195  projlem20 9200  projlem29 9209  cmbr3t 9546  cmcmt 9552  cmcm3t 9553  lecmt 9555  cnopct 9832  cnfnct 9849  0cnop 9898  0cnfn 9899  idcnop 9900  nmopunt 9934  nmcopexlem1 9946  nmcopexlem6 9951  lnopcon 9958  nmcfnexlem1 9975  nmcfnexlem6 9980  lnfncon 9985  nlelch 9989  branmfnt 10033  pjnmop 10070  hmopidmch 10074  pjnormss 10091  stge1 10160  strlem5 10177  hstrlem5 10185  mddmd 10231  csmdsym 10256  cvmdt 10258  elat 10261  cvbr3 10289  irredlem3 10314  irredlem4 10315  irredt 10317  atmd 10321  mdsymt 10334  mddmdin0 10353  cdj1 10355  cdj3 10363  inposet 10477

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 2053  df-sn 2416  df-pr 2417  df-op 2420  df-br 2625

Copyright terms: Public domain