Theorem breq1 2617

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 2483	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	eleq1d 1537	. 2 |- (A = B -> (<.A, C>. e. R <-> <.B, C>. e. R))
3		df-br 2615	. 2 |- (ARC <-> <.A, C>. e. R)
4		df-br 2615	. 2 |- (BRC <-> <.B, C>. e. R)
5	2, 3, 4	3bitr4g 554	1 |- (A = B -> (ARC <-> BRC))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954   e. wcel 956  <.cop 2407   class class class wbr 2614

This theorem is referenced by:  breq12 2619  breq1i 2621  breq1d 2624  brab1 2655  pocl 2839  solin 2852  so 2859  dffr2 2914  frirr 2919  dfwe2 2930  wereu 2940  vtoclr 3206  vtoclrbr 3207  vtoclibr 3208  ididg 3273  opelco 3283  opelcog 3285  opelcnvg 3291  eldm 3302  breldmg 3311  imasng 3416  asymref2 3432  coi1 3502  dffunmof 3522  fun11 3554  fneu 3584  fv2 3711  tz6.12-2 3730  ndmfv 3736  funbrfv 3741  fnbrfvb 3744  dff2 3808  f1fv 3865  isorel 3885  isocnv 3887  isotr 3888  isotrALT 3889  isomin 3890  isoini 3891  isowe 3894  f1oiso 3895  f1oweALT 3897  caoprord 4048  caoprord3 4050  ertr 4264  erref 4265  erth 4272  ecopoprsym 4300  ecopoprtrn 4301  th3qlem2 4305  ensymg 4398  en0 4410  en1 4413  endisj 4423  xpdom2 4428  sbth 4443  pwen 4489  ssenen 4490  nneneq 4498  php 4499  pssnn 4519  unifi 4538  fiint 4540  abfii3 4543  abfii4 4544  fodomfi 4546  iunfi 4549  supmo 4556  supub 4560  suplub 4561  supmaxlem 4568  suppr 4570  supsnALT 4572  unbnnt 4619  kardex 4705  karden 4706  hta 4708  aceq3lem 4712  numth2 4765  numthcor 4766  zorn2lem2 4769  zorn2lem3 4770  zorn2lem7 4774  zorn2 4776  brdom7disj 4784  brdom6disj 4785  uniimadom 4790  oncardval 4799  oncardid 4801  cardonle 4802  cardid 4808  oncard 4809  cardne 4810  iscard2 4834  ondomon 4836  ondomcard 4837  alephon 4845  alephsuc 4846  alephval2 4882  ltpiord 4995  ltsopq 5055  ltapq 5056  ltmpq 5057  ltexpq 5060  ltbtwnpq 5064  prcdpq 5077  prnmax 5079  genpnmax 5090  1pr 5097  1idpr 5113  prlem934 5119  reclem2pr 5137  reclem3pr 5138  reclem4pr 5139  recexpr 5140  supexpr 5143  ltsosr 5183  1ne0sr 5185  ltasr 5189  suppsr 5202  suppsr2 5203  supsrlem6 5210  supre 5240  ltsor 5241  pre-axltadd 5269  lelttrt 5504  xrltnsymt 5531  xrlttrit 5533  xrlttrt 5534  xrlelttrt 5543  nltpnftt 5547  ltadd1t 5605  leadd1t 5607  ltsubaddt 5609  lesubaddt 5611  lt2addt 5625  le2addt 5626  ltnegt 5636  lenegt 5638  ltmul1t 5794  ltdiv1t 5813  ltmuldivt 5825  ltrec 5835  lt2msq 5837  ltrect 5840  lerect 5841  lt2msqt 5842  le2msqt 5859  posex 5864  xrmaxltt 5869  maxlet 5874  maxltt 5878  nnleltp1t 5909  nnsubt 5912  nominpos 5998  lbreu 6000  lble 6002  lbinfm 6003  sup2 6006  infm3 6009  infmsup 6023  nnunb 6025  arch 6026  xrinfmexpnf 6030  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxr 6036  supxrre 6038  supxrunb1 6044  supxrunb2 6045  nn0ltp1let 6082  nn0subt 6116  zltp1let 6136  zextlet 6144  peano5uzt 6160  uzwo4OLD 6166  uzwo5OLD 6167  btwnz 6171  uzwo3lem2 6173  uzwo3 6174  zmax 6176  rebtwnz 6178  flvalt 6181  flleltt 6183  flval2t 6189  flval3t 6190  flbit 6192  qbtwnre 6224  qbtwnxr 6225  ser1add2 6283  ser1add 6284  ioovalt 6311  iocvalt 6320  icovalt 6321  iccvalt 6322  elioo1t 6323  elioo2t 6324  elioc1t 6327  elico1t 6328  elicc1t 6329  icoun 6354  snunioolem 6355  snunioo 6356  uzvalt 6359  uzwo 6395  uzwoOLD 6396  nnwof 6399  uzinfm 6402  fzvalt 6409  elfz1t 6410  fsequb2 6464  sqlecant 6580  sqrlem6 6616  sqrlem12 6622  sqrlem18 6628  sqrlem20 6630  sqrlet 6651  sqr2irrlem2 6663  sqr2irrlem3 6664  abslt 6818  absle 6819  absltOLD 6820  absleOLD 6821  absltt 6825  abslttOLD 6826  abslet 6827  seq1ublem 6856  seq1ub 6857  cau3i 6859  cau3ir 6860  cau5i 6862  cvg1 6866  cvg3 6868  cvganz 6869  faclbnd4lem1 6893  bcvalt 6903  bcpasc2t 6914  bccl2t 6917  dffsum 6944  fsumsplit 6966  clm3 7025  clm4 7026  climfnn 7038  climconst 7039  climuni 7044  climshft 7049  climshft2 7051  climaddlem3 7060  climmullem8 7071  climsup 7099  caucvglem1 7101  caucvglem2 7102  caucvglem5 7105  caucvg3t 7112  serzf0 7113  ser1f0 7114  ser1clim0 7117  cvgcmpub 7129  cvgcmp3cet 7134  expcnvlem1 7170  expcnvlem5 7174  expcnvlem6 7175  efaddlem25 7312  eflegeot 7364  efm1legeot 7366  reefiso 7378  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  unbenlem 7455  ruclem4 7464  ruclem33 7493  ruclem36 7496  unctb 7527  infmap2lem1 7529  subbas 7594  subbas2 7595  fctop 7600  qdensere 7701  ssblex 7808  tgioolem 7866  lmconst 7886  lmnn 7887  cmscvg 7898  lmfex 7910  metelcls 7916  metcn4i 7922  xplm 7925  xpcn 7926  iscms2lem4 7942  iscms2lem5 7943  bcthlem15 7963  nmoubi 8380  minveclem10 8498  spwmo 8598  pilem2 8610  pilem3 8611  logltbt 8715  chlim 9043  hlim0 9044  hlimcau 9046  hlimuni 9048  chcompl 9054  hsn0elch 9059  projlem8 9132  projlem13 9137  projlem28 9152  cmbr3t 9491  cmcmt 9497  cmcm3t 9498  lecmt 9500  nmopubt 9772  nmfnleubt 9788  nmopunt 9877  cnlnadjlem7 9944  bra11 9979  pjnmop 10013  stle0 10104  stles 10106  stm1 10108  csmdsym 10198  cvmdt 10200  atcveq0 10212  atcv1t 10244  atordt 10252  atcvat2t 10253  irredt 10259  mdsymt 10276  mddmdin0 10292  cdj1 10294  gelsupvalOLD 10354  infi1 10383  fine 10384  abfi 10385  ficli 10404  fipfil2 10475  filint2 10482  infi 10484  cnfilca 10487

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409  df-op 2412  df-br 2615

Copyright terms: Public domain