Theorem breq2 4134

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq2	⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 3905	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	eleq1d 2307	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3		df-br 4131	. 2 ⊢ (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4		df-br 4131	. 2 ⊢ (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ⟨cop 3712   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  breq12  4135  breq2i  4138  breq2d  4142  nbrne1  4149  brralrspcev  4189  brimralrspcev  4190  pocl  4448  swopolem  4450  swopo  4451  sowlin  4465  sotricim  4468  sotritrieq  4470  seex  4480  frind  4497  wetriext  4724  vtoclr  4823  posng  4847  brcog  4947  brcogw  4949  opelcnvg  4960  dfdmf  4974  breldmg  4987  dfrnf  5023  dmcoss  5052  resieq  5073  dfres2  5115  elimag  5130  elrelimasn  5153  elimasn  5154  intirr  5174  poirr2  5180  poltletr  5188  dffun6f  5390  dffun4f  5393  fun11  5448  brprcneu  5688  fv3  5718  tz6.12c  5725  relelfvdm  5727  fvmbr  5731  funbrfv  5739  fnbrfvb  5741  funfvdm2f  5768  fndmdif  5814  dff3im  5853  fmptco  5874  foeqcnvco  5996  isorel  6014  isocnv  6017  isotr  6022  isopolem  6028  isosolem  6030  f1oiso  6032  f1oiso2  6033  caovordig  6255  caovordg  6257  caovord  6261  caofrss  6334  caoftrn  6335  poxp  6468  tposoprab  6551  ertr  6822  ecopovsym  6905  ecopovtrn  6906  ecopovsymg  6908  ecopovtrng  6909  th3qlem2  6912  domeng  7036  eqeng  7052  snfig  7103  nneneq  7158  nnfi  7174  ssfilem  7177  ssfilemd  7179  domfiexmid  7182  dif1enen  7184  diffitest  7191  findcard  7192  findcard2  7193  findcard2s  7194  diffisn  7197  tridc  7204  fimax2gtrilemstep  7205  inffiexmid  7213  unsnfi  7226  fiintim  7238  fisseneq  7242  isbth  7284  supmoti  7334  eqsupti  7337  supubti  7340  suplubti  7341  suplub2ti  7342  supmaxti  7345  supsnti  7346  isotilem  7347  isoti  7348  supisolem  7349  supisoex  7350  cardcl  7527  isnumi  7528  cardval3ex  7531  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  papsym  7613  papcotr  7614  exmidapne  7627  nqtri3or  7764  ltsonq  7766  ltanqg  7768  ltmnqg  7769  ltexnqq  7776  nsmallnqq  7780  subhalfnqq  7782  ltbtwnnqq  7783  prarloclemarch2  7787  nqnq0pi  7806  prcdnql  7852  prcunqu  7853  prnminu  7857  genpcdl  7887  genprndl  7889  genprndu  7890  genpdisj  7891  nqprm  7910  nqprrnd  7911  nqprdisj  7912  nqprloc  7913  nqprlu  7915  nqprl  7919  addnqprlemru  7926  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemru  7942  mulnqprlemfl  7943  mulnqprlemfu  7944  1idpru  7959  ltnqpr  7961  ltnqpri  7962  prplnqu  7988  recexprlemelu  7991  recexprlemm  7992  recexprlemloc  7999  recexprlem1ssl  8001  recexprlemss1u  8004  cauappcvgprlemm  8013  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem2  8028  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem2  8048  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnbj  8061  caucvgprprlemmu  8063  caucvgprprlemexbt  8074  caucvgprprlemaddq  8076  caucvgprprlem1  8077  caucvgprprlem2  8078  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexpr  8093  lttrsr  8130  ltsosr  8132  ltasrg  8138  recexgt0sr  8141  mulgt0sr  8146  aptisr  8147  mulextsr1  8149  srpospr  8151  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  caucvgsr  8170  map2psrprg  8173  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axprecex  8248  axpre-ltwlin  8251  axpre-lttrn  8252  axpre-apti  8253  axpre-ltadd  8254  axpre-mulgt0  8255  axpre-mulext  8256  axcaucvglemcau  8266  axcaucvglemres  8267  axcaucvg  8268  axpre-suploclemres  8269  axpre-suploc  8270  ltxrlt  8392  lttri3  8406  ltne  8411  eqle  8418  ltordlem  8812  reapti  8910  apreim  8934  squeeze0  9237  lbreu  9278  lble  9280  suprleubex  9287  sup3exmid  9290  nnge1  9330  nn2ge  9340  nn1gt1  9341  nnsub  9346  nominpos  9548  nn0ge0  9593  elnnnn0b  9612  nn0ge2m1nn  9632  zdclt  9727  suprzclex  9749  peano2uz2  9758  peano5uzti  9759  dfuzi  9761  uzind  9762  uzind3  9764  eluz1  9935  uzind4  9998  indstr  10003  supinfneg  10005  infsupneg  10006  infregelbex  10008  indstr2  10019  ublbneg  10023  irraddap  10057  irrmulap  10059  elpq  10060  elpqb  10061  elrp  10067  mnfltxr  10199  nn0pnfge0  10204  xrltnsym  10206  xrlttr  10208  xrltso  10209  xrlttri3  10210  xrltne  10226  ngtmnft  10230  nmnfgt  10231  xrrebnd  10232  z2ge  10239  xltnegi  10248  xltadd1  10289  xsubge0  10294  xleaddadd  10300  ixxval  10309  elixx1  10310  elioo2  10334  iccid  10338  iccsupr  10379  repos  10383  fzval  10424  elfz1  10427  fzm1  10518  zsupcllemstep  10673  suprzubdc  10682  zsupssdc  10684  qdclt  10691  exbtwnzlemstep  10693  exbtwnzlemex  10695  qbtwnre  10702  qbtwnxr  10703  flval  10718  apbtwnz  10720  flaplt  10733  modqid2  10803  modqmuladdnn0  10820  exp3val  10993  expge0  11027  expge1  11028  nn0ltexp2  11163  facdiv  11192  facwordi  11194  hashinfom  11233  hashennn  11235  hashunlem  11260  zfz1iso  11309  wrdlen1  11358  fstwrdne0  11360  wrdl1exs1  11413  pfxsuffeqwrdeq  11486  pfxsuff1eqwrdeq  11487  ccats1pfxeq  11502  ccats1pfxeqrex  11503  pfxccatin12lem3  11520  ovshftex  11600  shftfibg  11601  shftfib  11604  shftfn  11605  2shfti  11612  sqrt0rlem  11785  resqrexlemex  11807  rsqrmo  11809  resqrtcl  11811  rersqrtthlem  11812  sqrtsq  11826  cau3lem  11897  caubnd2  11900  maxleim  11988  maxabslemval  11991  maxleast  11996  maxleb  11999  fimaxre2  12010  fiidxsupcl  12012  minmax  12014  xrmaxleim  12029  xrmaxiflemval  12035  xrmaxaddlem  12045  xrminmax  12050  xrbdtri  12061  climi  12072  climeu  12081  climmo  12083  2clim  12086  addcn2  12095  mulcn2  12097  reccn2ap  12098  cn1lem  12099  summodc  12169  zsumdc  12170  fsum3  12173  cvgratz  12318  ntrivcvgap0  12335  prodmodc  12364  zproddc  12365  fprodseq  12369  fprodntrivap  12370  sinltxirr  12547  dvdsabsb  12596  0dvds  12597  alzdvds  12640  dvdsext  12641  fzo0dvdseq  12643  2tp1odd  12670  2teven  12673  divalglemnn  12704  divalglemeunn  12707  divalglemeuneg  12709  bitsinv1lem  12747  gcdval  12755  gcddvds  12759  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlemex  12797  bezoutlemeu  12803  bezoutlemsup  12805  dfgcd3  12806  bezout  12807  dvdsgcd  12808  dfgcd2  12810  dvdssq  12827  uzwodc  12833  nnwofdc  12834  lcmval  12860  lcmcllem  12864  dvdslcm  12866  lcmledvds  12867  lcmgcdlem  12874  lcmdvds  12876  coprmgcdb  12885  coprmdvds2  12890  cncongr1  12900  cncongr2  12901  isprm  12906  dvdsnprmd  12922  dvdsprm  12935  exprmfct  12936  isprm6  12945  prmexpb  12949  prmfac1  12950  rpexp  12951  sqrt2irr  12960  nnmaxpwlemparts  12971  nnmaxpw  12972  sqpweven  12974  2sqpwodd  12975  sqne2sq  12976  nnoddn2prmb  13064  pceu  13097  pczpre  13099  pcdiv  13104  pcdvdsb  13122  difsqpwdvds  13140  pcmpt  13145  pcmptdvds  13147  oddprmdvds  13156  prmpwdvds  13157  infpnlem2  13162  ballotfilemfcc  13285  oddennn  13335  evenennn  13336  exmidunben  13369  nninfdclemcl  13391  nninfdclemp1  13393  nninfdc  13396  infpn2  13399  eqgen  14083  zndvds  15068  znleval  15072  psrmulvalfi  15160  comet  15691  metcnpi  15707  metcnpi2  15708  metcnpi3  15709  addcncntoplem  15753  cncfi  15770  elcncf1di  15771  mulcncflem  15799  dedekindeulemuub  15809  dedekindeulemloc  15811  dedekindeulemlu  15813  dedekindeulemeu  15814  dedekindeu  15815  suplociccreex  15816  suplociccex  15817  dedekindicclemuub  15818  dedekindicclemloc  15820  dedekindicclemlu  15822  dedekindicclemeu  15823  dedekindicclemicc  15824  dedekindicc  15825  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemloc  15833  ivthinc  15835  ivthreinc  15837  dich0  15844  ivthdich  15845  limcimo  15857  cnplimclemr  15861  limccnp2lem  15868  limccoap  15870  eldvap  15874  logltb  16068  zprmlogbaplem3  16178  zprmlogbap  16179  pellexlem3  16192  ppiublem1  16252  chtqub  16257  bpos1lem  16270  bposlem9  16280  lgsdir  16320  lgsne0  16323  gausslemma2dlem0i  16342  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  2lgslem2  16377  2lgs  16389  2sqlem6  16405  2sqlem8  16408  2sqlem10  16410  lfgredg2dom  16539  istrl  16792  clwwlkn0  16815  clwwlkext2edg  16829  clwwlknonccat  16840  clwwlknonex2  16846  iseupth  16854  konigsberg  16900  lealltlt2  16918  sbthom  17237  rirrdisj  17251  trilpo  17259  trirec0  17260  apdiff  17264  reap0  17275  cndcap  17276  nconstwlpolem  17282  neapmkv  17285  neap0mkv  17286  ltlenmkv  17287