Theorem breq2 3342

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 3159	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	eleq1d 1963	. 2 |- (A = B -> (<.C, A>. e. R <-> <.C, B>. e. R))
3		df-br 3339	. 2 |- (CRA <-> <.C, A>. e. R)
4		df-br 3339	. 2 |- (CRB <-> <.C, B>. e. R)
5	2, 3, 4	3bitr4g 614	1 |- (A = B -> (CRA <-> CRB))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298   e. wcel 1300  <.cop 3046   class class class wbr 3338

This theorem is referenced by:  breq12 3343  breq2i 3346  breq2d 3350  pocl 3596  posn 3603  solin 3612  sotric 3615  sotrieq 3616  sotrieqOLD 3617  so 3620  dffr2 3627  dffr2OLD 3628  frirr 3634  fr2nr 3635  wereu 3654  fr3nr 3859  dfwe2 3861  dfwe2OLD 3862  vtoclr 4032  vtoclrbrOLD 4034  vtoclibr 4035  ididgOLD 4118  opelco 4130  opelcoOLD 4131  opelco2g 4133  opelcnvg 4140  opelcnvgOLD 4141  dmcoss 4211  resieq 4227  elimag 4269  elimasn 4289  elinisegOLD 4295  asymref2 4310  asymref2OLD 4311  intirr 4312  dffun3 4432  dffun6f 4435  fun11 4480  fv3 4690  tz6.12c 4697  tz6.12i 4698  funbrfv 4709  fnbrfvb 4712  funbrfvbg 4716  funfv2f 4733  dffv2 4734  dff3 4790  isorel 4871  isocnv 4873  isotr 4874  isotrALT 4875  isowe 4880  f1oiso 4881  f1oweALT 4883  caoprord 4989  ertr 5332  erref 5333  elec 5337  ecopoprsym 5369  ecopoprtrn 5370  th3qlem2 5374  domeng 5439  eqeng 5451  ensymg 5470  snfi 5491  xpdom1g 5503  sbth 5520  nneneq 5606  php2 5608  onfin 5613  omsdomnn 5623  pssnn 5628  ssnnfi 5629  unfi 5644  unifi 5648  fiint 5650  fodomfi 5656  supmo 5666  supub 5670  suplub 5671  supmaxlem 5678  suppr 5680  supsnALT 5682  ordtypelem2 5685  ordtypelem6 5689  ordtypelem7 5690  ordtype 5691  onsdom 5694  hta 5858  oncardval 5865  omsubsuc 5877  omsubsuc2 5878  omsubsdomlem1 5879  elomsubsd 5885  omsubinit 5890  aceq3lem 5894  numth2 5947  zorn2lem2 5951  zorn2lem7 5956  zorn2 5958  fodomg 5961  brdom7disj 5966  brdom6disj 5967  unidomg 5971  cardval 5975  carden 5981  unxpdom 5996  sucxpdom 5998  cardlim 6003  cardmin 6012  alephnbtwn 6016  alephordlem1 6020  cardaleph 6033  alephval2 6050  dominf 6052  cdaeng 6074  ltpiord 6167  indpi 6186  ltsopq 6227  ltapq 6228  ltmpq 6229  ltexpq 6232  nsmallpq 6235  ltbtwnpq 6236  ltrpq 6237  prcdpq 6249  genpcd 6261  genpnmax 6262  prlem934b 6290  ltaddpr2 6293  ltexprlem4 6297  reclem3pr 6310  supexpr 6315  ltsosr 6355  ltasr 6361  recexsrlem 6364  mulgt0sr 6366  map2psrpr 6372  suppsrlem 6373  suppsr 6374  suppsr2 6375  suppsr3 6376  supsrlem5 6381  supsrlem6 6382  supre 6412  ltsor 6413  pre-axltadd 6442  pre-axmulgt0 6443  ltletr 6694  letr 6695  mnfltxr 6720  xrltnsym 6725  xrlttri 6727  xrlttr 6728  xrltletr 6738  xrletr 6739  ngtmnft 6742  eqle 6746  gt0ne0 6800  ltadd1 6806  leadd1 6808  ltsubadd 6810  lesubadd 6812  lt2add 6827  le2add 6828  addgt0OLD 6832  addgegt0OLD 6834  addge0OLD 6838  ltneg 6844  leneg 6846  lesub0 6867  mulge0 6868  mulge0OLD 6869  elimgt0 6987  elimge0 6988  prodgt0 7004  prodge0 7006  ltmul1 7008  ltdiv1 7031  ltdiv1OLD 7032  ltmuldiv 7045  ltmuldivOLD 7046  ltreci 7062  ltrec 7067  lerec 7068  lt2msq 7069  le2msq 7086  posexi 7091  xrltmin 7097  lemin 7104  squeeze0 7107  nn2ge 7125  nnge1 7126  nnleltp1 7138  nnsubi 7140  nnsub 7141  halfpos 7222  nominpos 7230  elrp 7233  lbreu 7254  lble 7256  lbinfm 7257  sup2 7260  infm3 7263  infmsup 7277  infmrcl 7278  nnunb 7279  xrsupexmnf 7283  xrsupsslem 7285  xrinfmsslem 7286  xrub 7289  supxr 7290  supxrre 7292  supxrpnf 7297  supxrunb1 7298  supxrunb2 7299  lt0nnn0 7325  nn0ltp1le 7336  elnnz1 7364  nn0sub 7370  zltp1le 7390  z2ge 7400  peano2uz2 7413  dfuzi 7414  uzind 7417  uzind3 7419  uzindOLD 7420  uzind3OLD 7421  uzwo4OLD 7422  uzwo5OLD 7423  uzwo3lem2 7430  uzwo3 7431  zmin 7432  zmax 7433  zbtwnre 7434  rebtwnz 7435  qbtwnre 7459  qbtwnxr 7460  flval 7464  flval2 7478  flval3 7479  modid2 7513  monoord 7523  iooval 7533  iocval 7542  icoval 7543  iccval 7544  elioo1 7545  elioo2 7546  elioc1 7548  elico1 7549  elicc1 7550  iccsupr 7567  repos 7568  icoun 7582  snunioo 7584  eluz1 7589  uzind4 7619  uzwo 7624  uzwoOLD 7625  nnwof 7628  fzval 7639  elfz1 7640  fzsuc 7678  fsequb 7702  om2uzuzi 7708  om2uzrani 7711  uzrdginii 7715  uzrdginip1i 7717  seqzval 7783  seqz1 7790  sq11 7874  sqrval 7921  sqr0 7922  sqrlem4 7926  sqrlem6 7928  sqrlem12 7934  sqrlem13 7935  sqrlem20 7942  sqrlem21 7943  sqrlem22 7944  sqrlem24 7946  sqrgt0ii 7947  sqrlem26 7948  sqrcl 7960  sqrgt0 7961  sqrge0 7962  sqrle 7963  sqr00 7964  sqrsq 7972  sqsqr 7973  sqr2irrlem1 7974  sqr2irrlem2 7975  sqr2irr 7979  absid 8113  abslt 8132  absle 8133  abs3lem 8159  seq1bndi 8162  cau3ii 8166  cau3iri 8167  cvg2i 8174  caubndi 8178  facdiv 8194  facwordi 8196  bcval 8210  bcpasc2 8220  bccl2 8223  dffsum 8258  clm4lei 8341  clmi1i 8346  climuni 8359  climeu 8360  2climnn 8362  2climnn0 8363  climshfti 8364  iserzshft2i 8367  climrecl 8370  climge0 8372  climaddlem3 8376  climmullem8 8387  iserzex 8395  climcmplem 8397  iserzexi 8406  climubii 8413  climsupi 8415  climcaui 8416  caucvglem2 8418  caucvglem6 8422  caucvgi 8423  caucvg2i 8425  caucvg3lem 8426  caucvg3 8428  serzf0i 8429  ser1cmp2i 8437  cvgcmp2lem 8440  cvgcmpubi 8446  cvgcmp3cei 8448  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  isumclimtfi 8456  isumspliti 8477  infcvglem1 8482  expcnvlem3 8490  expcnvlem5 8492  geoisum1c 8507  cvgratlem1ALT 8509  cvgratlem1 8512  cvgratlem4 8515  elcncf1di 8532  ivthlem2 8544  efseq1ex 8568  efseq0ex 8573  efaddlem24 8623  eflegeo 8681  efm1legeo 8683  efcnlem4 8687  efcn 8688  reeff1olem2 8690  reefiso 8693  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  unbenlem 8773  infpnlem2 8776  infpn2 8778  ruclem4 8782  ruclem33 8811  ruclem35 8813  ruclem36 8814  infxpidmlem2 8822  infxpidmlem3 8823  infxpidmlem8 8828  infmap2 8850  qdensere 9027  metxp 9111  blfval2 9113  blval 9114  blrn2 9119  blelrn 9125  blin 9129  blss 9130  ssblex 9133  opnin 9146  blnei 9156  metcnp 9165  metcnpi 9168  metcnpi2 9169  metcnpi3 9170  metcnpi4 9171  metcni 9172  metcni2 9173  tgioolem 9192  lmcvg 9210  iscau3 9216  iscau4 9218  caun0 9223  lmuni 9229  lmle 9238  metelcls 9243  metcnp4 9248  metcn4i 9250  xpcn 9254  lmcau 9274  bcthlem2 9278  bcthlem4 9280  bcthlem12 9288  bcthlem14 9290  bcthlem15 9291  bcthlem18 9294  bcthlem32 9308  gxval 9381  gapm 9462  vacnlem3 9669  nmcnilem 9676  va1cnlem 9684  sm1cnilem 9686  nmobndi 9777  blocni 9805  ubthlem1 9872  ubthlem14 9887  minveclem10 9899  minveclem27 9916  htthlem7 9973  spwmo 9999  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  pilem2 10021  pilem3 10022  pilem4 10023  sinhalfpilem 10028  efifolem5 10080  efif1lem5 10088  logltb 10130  dif1en 10172  dif1enOLD 10173  indexfi 10174  ficard 10176  dif1card 10177  findcard 10178  dirtr 10356  tosdir 10358  axhcompl 10500  norm3lemt 10652  hcau2 10688  chlimi 10737  hlimcauii 10739  hlimcaui 10740  hlimuniii 10741  hlimunii 10742  hlimreui 10743  hlimeui 10744  occllem6 10811  occllem8 10813  projlem1 10819  projlem7 10825  projlem8 10826  projlem15 10833  projlem20 10838  projlem29 10847  cmbr3 11184  cmcm 11190  cmcm3 11191  lecm 11193  cnopc 11474  cnfnc 11491  0cnop 11540  0cnfn 11541  idcnop 11542  nmopun 11576  nmcopexlem1 11588  nmcopexlem6 11593  lnopconi 11600  nmcfnexlem1 11617  nmcfnexlem6 11622  lnfnconi 11627  nlelchi 11631  branmfn 11675  branmfnOLD 11676  opsqrlem1 11711  pjnmopi 11719  hmopidmchi 11723  pjnormssi 11740  stge1i 11810  strlem5 11827  hstrlem5 11835  mddmd2 11881  csmdsymi 11906  cvmd 11908  ela 11911  cvbr3i 11939  irredlem3 11964  irredlem4 11965  irred 11967  atmd 11971  mdsym 11984  mddmdin0i 12003  cdj1i 12005  cdj3i 12013  bnj112 12457  bnj1185 12967  bnj602 13303  bnj1228 13456  bnj1482 13551  ublbneg 13653  suprzcl 13658  dvdsabsb 13674  0dvds 13675  dvdsle 13693  dvdsleabs 13694  alzdvds 13695  divalglem10 13705  gcdval 13715  gcdcllem1 13718  gcdcllem2 13719  gcddvds 13722  isprm 13768  isprm2lem 13774  epelg 13827  frirrc 13833  fundmpss 13836  predbrg 13897  poxp 13949  frxp 13951  poseq 13954  axdenselem4 14022  axdenselem5 14023  axdense 14027  nocvxminlem 14028  axfelem8 14038  axfelem10 14040  axfelem13 14043  axfelem15 14045  brtxp 14067  fnbigcup 14075  elfix 14077  srefwref 14373  infxpg 14422  infsdomnng 14423  puub2 14600  puub 14601  supdef 14604  ismnl2 14610  defge3 14613  inposet 14620  rngsubpos 14636  dffprod 14670  cntrsetlem 14999  domleqt 15020  lvsovso 15038  tarval 15212  tarvalg 15213  tarval1 15214  tarval1g 15215  tclinf 15241  trer 15361  elicc3 15362  ccid 15363  finminlem 15367  finsschain 15373  ordtypelem2OLD 15376  ordtypelem6OLD 15380  ordtypelem7OLD 15381  ordtypeOLD 15382  onsdomOLD 15385  omsubsucOLD 15386  omsubsuc2OLD 15387  omsubsdomlem1OLD 15388  elomsubsdOLD 15394  omsubinitOLD 15399  fneerdm 15498  topfneec 15501  fnessref 15503  refssfne 15504  fnemeet2 15529  fcluscomplem 15620  eltail 15635  filnetlem3 15642  xpeng 15691  erthdmg 15730  findcard2 15745  fimax 15746  fisupg 15748  indexfiOLD 15755  frinfm 15758  fisup2g 15768  frfi 15771  frminex 15773  add20 15777  fdc1 15813  nninfnub 15819  fsumltisumi 15823  fsumleisumi 15826  geomcau 15849  caushft 15851  metdcn 15853  oprpiece1res2 15881  haustlmu 15906  lmtlm 15908  txmet 15925  ismtyhmeolem 15950  heiborlem16 15970  heiborlem36 15990  bfplem8 16005  bfp 16009  recms 16010  rrncms 16019  phtpcdm 16061  ertr2 16257  erreft 16259  xrltneNEW 16434  dfstruct2 16709  fnelstr 16717  strdif 16719  poslem 16774  posasymb 16776  pleval2 16785  plttr 16790  pltletr 16791  lubprop 16805  lubid 16807  glbprop 16810  glble 16813  joinlem 16817  joinle 16820  meetlem 16824  meetle 16827  lubl 16896  lubun 16899  lubunNEW 16900  oposlem 16913  glb0 16920  omllaw 16964  cvrval 16988  cvrnbtwn 16990  cvrnbtwn2 16992  cvrnbtwn3 16993  cvrcon3b 16994  cvrnbtwn4 16996  cvrcmp 16999  isatom 17001  atnlt 17009  atlatex 17013  glbcon 17028  hlexch 17034  hlexchb 17035  hlatexch1 17045  cvratlem 17061  cvrat4 17076  ps-1 17078  pmapval 17237  pmapglbx 17251

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339

Copyright terms: Public domain