Theorem breq1 3341

Description: Equality theorem for a binary relation.

Assertion

Ref	Expression
breq1	|- (A = B -> (ARC <-> BRC))

Proof of Theorem breq1

Step	Hyp	Ref	Expression
1		opeq1 3158	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	eleq1d 1963	. 2 |- (A = B -> (<.A, C>. e. R <-> <.B, C>. e. R))
3		df-br 3339	. 2 |- (ARC <-> <.A, C>. e. R)
4		df-br 3339	. 2 |- (BRC <-> <.B, C>. e. R)
5	2, 3, 4	3bitr4g 614	1 |- (A = B -> (ARC <-> BRC))

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  breq1i 3345  breq1d 3348  brab1 3384  brab1OLD 3385  pocl 3596  posn 3603  solin 3612  sotrieq 3616  so 3620  dffr2OLD 3628  frirr 3634  wereu 3654  dfwe2 3861  dfwe2OLD 3862  vtoclr 4032  vtoclrbrOLD 4034  vtoclibr 4035  ididgOLD 4118  opelco 4130  opelcoOLD 4131  opelco2g 4133  opelcnvg 4140  opelcnvgOLD 4141  eldm 4153  breldmg 4162  imasng 4287  asymref2 4310  asymref2OLD 4311  coi1 4413  dffun6f 4435  fun11 4480  fneu 4517  fneuOLD 4518  fv2OLD 4677  tz6.12-2 4696  ndmfv 4702  nfunsn 4706  nfunsnOLD 4707  funbrfv 4709  fnbrfvb 4712  dffv2 4734  dff3 4790  dff13 4850  isorel 4871  isocnv 4873  isotr 4874  isotrALT 4875  isomin 4876  isoini 4877  isowe 4880  f1oiso 4881  f1oweALT 4883  caoprord 4989  caoprord3 4991  ertr 5332  erref 5333  erth 5340  ecopoprsym 5369  ecopoprtrn 5370  th3qlem2 5374  isfi 5441  ensymg 5470  en0 5482  en1 5485  endisj 5496  xpdom2 5501  sbth 5520  pwne 5552  2pwne 5553  pwen 5597  ssenen 5598  nneneq 5606  php 5607  pssnn 5628  unifi 5648  fiint 5650  fodomfi 5656  supmo 5666  supub 5670  suplub 5671  supmaxlem 5678  suppr 5680  supsnALT 5682  ordtypelem2 5685  ordtypelem3 5686  ordtypelem6 5689  ordtypelem7 5690  ordtype 5691  hartog 5693  onsdom 5694  unbnn3 5746  kardex 5855  karden 5856  hta 5858  oncardval 5865  oncardid 5867  cardonle 5868  alephon 5876  omsubsuc 5877  omsubsuc2 5878  omsublim 5887  infenomsub 5889  omsubinit 5890  aceq3lem 5894  numth2 5947  numthcor 5948  zorn2lem2 5951  zorn2lem3 5952  zorn2lem7 5956  zorn2 5958  brdom7disj 5966  brdom6disj 5967  uniimadom 5972  cardid 5977  oncard 5978  cardne 5980  iscard2 6006  ondomon 6008  ondomcard 6009  alephsuc 6014  alephval2 6050  cdaeng 6074  ltpiord 6167  ltsopq 6227  ltapq 6228  ltmpq 6229  ltexpq 6232  ltbtwnpq 6236  prcdpq 6249  prnmax 6251  genpnmax 6262  1pr 6269  1idpr 6285  prlem934 6291  reclem2pr 6309  reclem3pr 6310  reclem4pr 6311  recexpr 6312  supexpr 6315  ltsosr 6355  1ne0sr 6357  ltasr 6361  suppsr 6374  suppsr2 6375  supsrlem6 6382  supre 6412  ltsor 6413  pre-axltadd 6442  lelttr 6693  xrltnsym 6725  xrlttri 6727  xrlttr 6728  xrlelttr 6737  nltpnft 6741  ltadd1 6806  leadd1 6808  ltsubadd 6810  lesubadd 6812  lt2add 6827  le2add 6828  ltneg 6844  leneg 6846  ltmul1 7008  ltdiv1 7031  ltdiv1OLD 7032  ltmuldiv 7045  ltmuldivOLD 7046  ltreci 7062  lt2msqi 7064  ltrec 7067  lerec 7068  lt2msq 7069  le2msq 7086  posexi 7091  xrmaxlt 7096  maxle 7101  maxlt 7105  nnleltp1 7138  nnsub 7141  nominpos 7230  lbreu 7254  lble 7256  lbinfm 7257  sup2 7260  infm3 7263  infmsup 7277  nnunb 7279  arch 7280  xrinfmexpnf 7284  xrsupsslem 7285  xrinfmsslem 7286  xrub 7289  supxr 7290  supxrre 7292  supxrunb1 7298  supxrunb2 7299  nn0ltp1le 7336  nn0sub 7370  zltp1le 7390  zextle 7401  peano5uzti 7416  uzwo4OLD 7422  uzwo5OLD 7423  btwnz 7428  uzwo3lem2 7430  uzwo3 7431  zmax 7433  rebtwnz 7435  qbtwnre 7459  qbtwnxr 7460  flval 7464  fllelt 7467  flval2 7478  flval3 7479  flbi 7480  modid2 7513  iooval 7533  iocval 7542  icoval 7543  iccval 7544  elioo1 7545  elioo2 7546  elioc1 7548  elico1 7549  elicc1 7550  icoun 7582  snunioolem 7583  snunioo 7584  uzval 7588  uzwo 7624  uzwoOLD 7625  nnwof 7628  uzinfmi 7631  fzval 7639  elfz1 7640  fsequb2 7703  ser1add2i 7751  ser1addi 7752  sqlecan 7887  sqrlem6 7928  sqrlem12 7934  sqrlem18 7940  sqrlem20 7942  sqrle 7963  sqr2irrlem2 7975  sqr2irrlem3 7976  abslti 8127  abslei 8128  abslt 8132  absle 8133  seq1ublem 8163  seq1ubi 8164  cau3ii 8166  cau3iri 8167  cau5ii 8169  cvg1 8173  cvg3i 8175  cvganz 8176  faclbnd4lem1 8200  bcval 8210  bcpasc2 8220  bccl2 8223  dffsum 8258  fsumsplit 8280  clm3i 8339  clm4i 8340  climfnn 8352  climconsti 8354  climuni 8359  climshfti 8364  climshft2i 8366  climaddlem3 8376  climmullem8 8387  climsupi 8415  caucvglem1 8417  caucvglem2 8418  caucvglem5 8421  caucvg3 8428  serzf0i 8429  ser1clim0 8433  cvgcmpubi 8446  cvgcmp3ce 8451  expcnvlem1 8488  expcnvlem5 8492  expcnvlem6 8493  efaddlem25 8624  eflegeo 8681  efm1legeo 8683  reefiso 8693  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  unbenlem 8773  ruclem4 8782  ruclem33 8811  ruclem36 8814  infpss 8843  unctb 8846  infmap2lem1 8848  qdensere 9027  ssblex 9133  tgioolem 9192  lmconst 9212  lmnn 9213  cmscvg 9225  lmfex 9237  metelcls 9243  metcn4i 9250  xplm 9253  xpcn 9254  iscms2lem4 9270  iscms2lem5 9271  bcthlem15 9291  gapmlem 9461  vacnlem3 9669  vacnlem4 9670  nmoubi 9774  minveclem10 9899  spwmo 9999  spwpr2 10001  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  pilem2 10021  pilem3 10022  logltb 10130  dif1enOLD 10173  indexfi 10174  dif1card 10177  findcard 10178  dirtr 10356  dirge 10357  on1el4 10413  uznzr 10416  chlimi 10737  hlim0 10738  hlimcaui 10740  hlimunii 10742  chcompl 10748  hsn0elch 10753  projlem8 10826  projlem13 10831  projlem28 10846  cmbr3 11184  cmcm 11190  cmcm3 11191  lecm 11193  nmopub 11469  nmfnleub 11486  nmopun 11576  cnlnadjlem7 11643  bra11 11679  pjnmopi 11719  stle0i 11811  stlesi 11813  stm1i 11815  csmdsymi 11906  cvmd 11908  atcveq0 11920  atcv1 11952  atord 11960  atcvat2 11961  irred 11967  mdsym 11984  mddmdin0i 12003  cdj1i 12005  bnj36 12405  bnj39 12410  bnj1185 12967  bnj1152 13437  bnj1418 13529  fzind 13610  ublbneg 13653  lbzbi 13657  nn0seqcvgd 13659  absdvdsb 13673  dvdsle 13693  divalglem8 13703  divalglem9 13704  divalglem10 13705  divalgmod 13709  ndvdssub 13710  gcdcllem1 13718  gcdcllem2 13719  gcdcllem3 13720  algcvgblem 13745  1nprm 13769  1idssfct 13770  isprm2lem 13774  isprm2 13775  3prm 13780  4nprm 13781  coprm 13782  frirrc 13833  predbrg 13897  trclpred 13934  poxp 13949  frxp 13951  poseq 13954  axdense 14027  nocvxminlem 14028  axfelem9 14039  axfelem10 14040  axfelem13 14043  axfelem15 14045  brsset 14069  brbigcup 14074  imgfldref2 14368  srefwref 14373  prj1 14395  supdef 14604  supdefa 14605  ismxl2 14609  defse3 14614  inposet 14620  dfdir2 14639  dffprod 14670  top1 14896  top2ind 14897  top2usne 14898  cntrsetlem 14999  supnuf 15041  tarax3 15218  empistar 15219  cptarc 15242  fnctartar 15284  fnctartar2 15285  trer 15361  elicc3 15362  ccid 15363  finminlem 15367  finsschain 15373  ordtypelem2OLD 15376  ordtypelem3OLD 15377  ordtypelem6OLD 15380  ordtypelem7OLD 15381  ordtypeOLD 15382  hartogOLD 15384  onsdomOLD 15385  omsubsucOLD 15386  omsubsuc2OLD 15387  omsublimOLD 15396  infenomsubOLD 15398  omsubinitOLD 15399  reconnlem4 15449  2ndcsb 15476  2ndc1stc 15477  2ndcctbss 15478  topfneec 15501  fnejoin2 15531  fcluscomplem 15620  istail 15634  xpeng 15691  findcard2 15745  fimax 15746  indexdom 15754  indexfiOLD 15755  frfi 15771  filbcmb 15776  fdc 15812  caushft 15851  oprpiece1res1 15880  oprpiece1res2 15881  piececn 15894  totbndbnd 15944  heiborlem13 15967  heiborlem16 15970  heiborlem18 15972  heiborlem35 15989  heiborlem40 15994  bfp 16009  rrncms 16019  phtpycolem1 16051  phtpycolem2 16052  pcoval1 16074  pcoval2 16075  pcohtpylem1 16080  pcohtpylem2 16081  pcopt 16084  pcoass 16085  pcorev 16087  ertr2 16257  erreft 16259  poslem 16774  posasymb 16776  pltval3 16787  lubprop 16805  luble 16806  lubid 16807  glbprop 16810  joinval2 16816  joinlem 16817  meetval2 16823  meetlem 16824  lubub 16895  lubun 16899  lubunNEW 16900  clatleglb 16903  oposlem 16913  glb0 16920  omllaw 16964  cmtbr4 16976  cvrval 16988  cvrnbtwn 16990  cvrnbtwn2 16992  cvrnbtwn3 16993  cvrcon3b 16994  cvrnbtwn4 16996  atomcvreq0 17010  atomnle 17016  glbcon 17028  atomnlej1 17030  atomnlej2 17031  hlsuprexch 17033  hlatmstc 17047  hl2atom 17053  cvratlem 17061  atcvrj0 17065  atcvrj2b 17069  cvrat4 17076  ps2 17079  psubspi 17228  linepsub 17232  elpmap 17238  pmapsub 17250  elpadd 17260  paddvaln0 17262  paddasslem5 17285

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