Theorem breq2 2613

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 2479	. . 3 ⊢ (A = B → ⟨C, A⟩ = ⟨C, B⟩)
2	1	eleq1d 1532	. 2 ⊢ (A = B → (⟨C, A⟩ ∈ R ↔ ⟨C, B⟩ ∈ R))
3		df-br 2610	. 2 ⊢ (CRA ↔ ⟨C, A⟩ ∈ R)
4		df-br 2610	. 2 ⊢ (CRB ↔ ⟨C, B⟩ ∈ R)
5	2, 3, 4	3bitr4g 553	1 ⊢ (A = B → (CRA ↔ CRB))

Syntax hints:   → wi 3   ↔ wb 146   = wceq 953   ∈ wcel 955  ⟨cop 2401   class class class wbr 2609

This theorem is referenced by:  breq12 2614  breq2i 2617  breq2d 2620  pocl 2835  solin 2848  sotric 2851  sotrieq 2852  so 2855  dffr2 2909  frirr 2914  fr2nr 2915  fr3nr 2916  dfwe2 2925  wereu 2935  vtoclr 3201  vtoclrbr 3202  vtoclibr 3203  ididg 3268  opelco 3277  opelcog 3279  opelcnvg 3285  resieq 3360  elimag 3391  eliniseg 3413  asymref2 3424  asymref2OLD 3426  dffun3 3513  dffunmof 3516  fun11 3548  fv3 3718  tz6.12c 3725  tz6.12i 3726  funbrfv 3735  fnbrfvb 3738  funbrfvbg 3742  funfv2f 3757  dff2 3802  isorel 3879  isocnv 3881  isotr 3882  isotrALT 3883  isowe 3888  f1oiso 3889  f1oweALT 3891  caoprord 4042  ertr 4258  erref 4259  elec 4263  ecopoprsym 4294  ecopoprtrn 4295  th3qlem2 4299  domeng 4362  eqeng 4373  ensymg 4392  snfi 4413  xpdom1g 4424  sbth 4437  nneneq 4492  php2 4494  php3 4495  onfin 4499  ominf 4508  omsdomnn 4509  pssnn 4513  ssnn 4514  ssfi 4515  unfi 4528  unifi 4532  fiint 4534  abfii4 4538  fodomfi 4540  pwfi 4545  supmo 4550  supub 4554  suplub 4555  suppr 4562  supsnALT 4564  hta 4700  aceq3lem 4704  numth2 4757  zorn2lem2 4761  zorn2lem7 4766  zorn2 4768  fodomg 4771  brdom7disj 4776  brdom6disj 4777  unidomg 4781  oncardval 4791  cardval 4798  carden 4803  unxpdom 4816  sucxpdom 4818  cardlim 4823  cardmin 4832  alephnbtwn 4840  alephordlem1 4844  cardaleph 4857  alephval2 4874  dominf 4876  ltpiord 4987  indpi 5006  ltsopq 5047  ltapq 5048  ltmpq 5049  ltexpq 5052  nsmallpq 5055  ltbtwnpq 5056  ltrpq 5057  prcdpq 5069  genpcd 5081  genpnmax 5082  prlem934b 5110  ltaddpr2 5113  ltexprlem4 5117  reclem3pr 5130  supexpr 5135  ltsosr 5175  ltasr 5181  recexsrlem 5184  mulgt0sr 5186  map2psrpr 5192  suppsrlem 5193  suppsr 5194  suppsr2 5195  suppsr3 5196  supsrlem5 5201  supsrlem6 5202  supre 5232  ltsor 5233  pre-axltadd 5261  pre-axmulgt0 5262  ltletrt 5497  letrt 5498  pnfnemnf 5509  mnfltxrt 5518  xrltnsymt 5523  xrlttrit 5525  xrlttrt 5526  xrltletrt 5536  xrletrt 5537  ngtmnftt 5540  eqlet 5544  gt0ne0t 5592  ltadd1t 5597  leadd1t 5599  ltsubaddt 5601  lesubaddt 5603  lt2addt 5617  le2addt 5618  addgt0t 5620  addgegt0t 5621  addge0t 5623  ltnegt 5628  lenegt 5630  lesub0t 5651  mulge0t 5652  elimgt0 5765  elimge0 5766  prodgt0t 5782  prodge0t 5784  ltmul1t 5786  ltdiv1t 5805  ltmuldivt 5817  ltrec 5827  ltrect 5832  lerect 5833  lt2msqt 5834  le2msqt 5851  posex 5856  xrltmint 5862  lemint 5869  squeeze0 5872  nn2get 5890  nnge1t 5891  nnleltp1t 5901  nnsub 5903  nnsubt 5904  halfpost 5983  nominpos 5990  lbreu 5992  lble 5994  lbinfm 5995  sup2 5998  infm3 6001  infmsup 6015  infmrcl 6016  nnunb 6017  xrsupexmnf 6021  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxr 6028  supxrre 6030  supxrpnf 6035  supxrunb1 6036  supxrunb2 6037  lt0nnn0 6063  nn0ltp1let 6074  elnnz1 6102  nn0subt 6108  zltp1let 6128  z2get 6135  peano2uz2 6149  dfuz 6150  uzind 6153  uzind3 6155  uzindOLD 6156  uzind3OLD 6157  uzwo4OLD 6158  uzwo5OLD 6159  uzwo3lem2 6165  uzwo3 6166  zmin 6167  zmax 6168  zbtwnre 6169  rebtwnz 6170  flvalt 6173  flval2t 6181  flval3t 6182  qbtwnre 6216  qbtwnxr 6217  elrp 6220  monoord 6231  om2uzuz 6234  om2uzran 6237  uzrdgini 6240  uzrdginip1 6242  ioovalt 6303  iocvalt 6312  icovalt 6313  iccvalt 6314  elioo1t 6315  elioo2t 6316  elioc1t 6319  elico1t 6320  elicc1t 6321  iccsupr 6331  repos 6332  icoun 6346  snunioo 6348  eluz1t 6352  uzind4 6382  uzwo 6387  uzwoOLD 6388  nnwof 6391  fzvalt 6401  elfz1t 6402  fsequb 6455  seqzvalt 6472  seqz1 6479  sq11t 6560  sqrval 6601  sqr0 6602  sqrlem4 6606  sqrlem6 6608  sqrlem12 6614  sqrlem13 6615  sqrlem20 6622  sqrlem21 6623  sqrlem22 6624  sqrlem24 6626  sqrgt0i 6627  sqrlem26 6628  sqrclt 6640  sqrgt0t 6641  sqrge0t 6642  sqrlet 6643  sqr00t 6644  sqrsqt 6652  sqsqrt 6653  sqr2irrlem1 6654  sqr2irrlem2 6655  sqr2irr 6659  absidt 6797  absltt 6817  abslttOLD 6818  abslet 6819  abs3lemt 6844  seq1bnd 6847  cau3i 6851  cau3ir 6852  cvg2 6859  caubnd 6863  facdivt 6879  facwordit 6881  bcvalt 6895  bcpasc2t 6906  bccl2t 6909  dffsum 6936  clm4le 7019  clmi1 7024  climuni 7036  climeu 7037  2climnn 7039  2climnn0 7040  climshft 7041  iserzshft2 7044  climrecl 7047  climge0 7049  climaddlem3 7052  climmullem8 7063  iserzext 7071  climcmplem 7073  iserzex 7082  climubi 7089  climsup 7091  climcau 7092  caucvglem2 7094  caucvglem6 7098  caucvg 7099  caucvg2 7101  caucvg3lem 7102  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1cmp2 7113  cvgcmp2lem 7116  cvgcmpub 7121  cvgcmp3ce 7123  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  isumclimtf 7131  isumsplit 7151  infcvglem1 7156  expcnvlem3 7164  expcnvlem5 7166  geoisum1c 7180  cvgratlem1ALT 7182  cvgratlem1 7185  cvgratlem4 7188  elcncf1d 7205  ivthlem2 7217  ivthlem4OLD 7228  efseq1ex 7248  efseq0ex 7253  efaddlem24 7303  eflegeot 7356  efm1legeot 7358  efcnlem4 7362  efcn 7363  reeff1olem2 7365  reeff1olem2OLD 7367  reefiso 7370  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  unbenlem 7447  infpnlem2 7450  infpn2 7452  ruclem4 7456  ruclem33 7485  ruclem35 7487  ruclem36 7488  infxpidmlem2 7496  infxpidmlem3 7497  infxpidmlem8 7502  infmap2 7523  qdensere 7691  metxp 7774  blfval2 7776  blval 7777  blrn2 7782  blelrn 7788  blin 7792  blss 7793  ssblex 7796  opnin 7809  blnei 7818  metcnp 7826  metcnpi 7829  metcnpi2 7830  metcnpi3 7831  metcnpi4 7832  metcni 7833  metcni2 7834  tgioolem 7853  lmcvg 7870  iscau3 7876  caun0 7880  lmuni 7886  lmle 7895  metelcls 7900  metcnp4 7904  metcn4i 7906  xpcn 7910  lmcau 7930  bcthlem2 7934  bcthlem4 7936  bcthlem12 7944  bcthlem14 7946  bcthlem15 7947  bcthlem18 7950  bcthlem32 7964  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  nmobndi 8370  blocni 8396  ubthlem1 8460  ubthlem14 8473  minveclem10 8485  minveclem27 8502  htthlem7 8556  spwmo 8580  pilem2 8591  pilem3 8592  pilem4 8593  sinhalfpilem 8598  efifolem5 8641  efif1lem5 8649  logltbt 8698  logltbtOLD 8715  norm3lemt 8940  hcau2 8976  chlim 9025  hlimcaui 9027  hlimcau 9028  hlimunii 9029  hlimuni 9030  hlimreu 9031  hlimeu 9032  occllem6 9094  occllem8 9096  projlem1 9102  projlem7 9108  projlem8 9109  projlem15 9116  projlem20 9121  projlem29 9130  cmbr3t 9468  cmcmt 9474  cmcm3t 9475  lecmt 9477  cnopct 9753  cnfnct 9770  0cnop 9819  0cnfn 9820  idcnop 9821  nmopunt 9854  nmcopexlem1 9866  nmcopexlem6 9871  lnopcon 9878  nmcfnexlem1 9895  nmcfnexlem6 9900  lnfncon 9905  nlelch 9909  branmfnt 9951  pjnmop 9986  hmopidmch 9990  pjnormss 10007  stge1 10075  strlem5 10092  hstrlem5 10100  mddmd 10144  csmdsym 10169  cvmdt 10171  elat 10174  cvbr3 10202  irredlem3 10227  irredlem4 10228  irredt 10230  atmd 10234  mdsymt 10247  mddmdin0 10263  cdj1 10265  cdj3 10273  infi 10448

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain