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  7333  eqsupti  7336  supubti  7339  suplubti  7340  suplub2ti  7341  supmaxti  7344  supsnti  7345  isotilem  7346  isoti  7347  supisolem  7348  supisoex  7349  cardcl  7526  isnumi  7527  cardval3ex  7530  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  papsym  7612  papcotr  7613  exmidapne  7626  nqtri3or  7763  ltsonq  7765  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  nsmallnqq  7779  subhalfnqq  7781  ltbtwnnqq  7782  prarloclemarch2  7786  nqnq0pi  7805  prcdnql  7851  prcunqu  7852  prnminu  7856  genpcdl  7886  genprndl  7888  genprndu  7889  genpdisj  7890  nqprm  7909  nqprrnd  7910  nqprdisj  7911  nqprloc  7912  nqprlu  7914  nqprl  7918  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  1idpru  7958  ltnqpr  7960  ltnqpri  7961  prplnqu  7987  recexprlemelu  7990  recexprlemm  7991  recexprlemloc  7998  recexprlem1ssl  8000  recexprlemss1u  8003  cauappcvgprlemm  8012  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem2  8027  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem2  8047  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnbj  8060  caucvgprprlemmu  8062  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexpr  8092  lttrsr  8129  ltsosr  8131  ltasrg  8137  recexgt0sr  8140  mulgt0sr  8145  aptisr  8146  mulextsr1  8148  srpospr  8150  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  map2psrprg  8172  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axprecex  8247  axpre-ltwlin  8250  axpre-lttrn  8251  axpre-apti  8252  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  axcaucvglemcau  8265  axcaucvglemres  8266  axcaucvg  8267  axpre-suploclemres  8268  axpre-suploc  8269  ltxrlt  8391  lttri3  8405  ltne  8410  eqle  8417  ltordlem  8811  reapti  8909  apreim  8933  squeeze0  9236  lbreu  9277  lble  9279  suprleubex  9286  sup3exmid  9289  nnge1  9329  nn2ge  9339  nn1gt1  9340  nnsub  9345  nominpos  9547  nn0ge0  9592  elnnnn0b  9611  nn0ge2m1nn  9631  zdclt  9726  suprzclex  9748  peano2uz2  9757  peano5uzti  9758  dfuzi  9760  uzind  9761  uzind3  9763  eluz1  9934  uzind4  9997  indstr  10002  supinfneg  10004  infsupneg  10005  infregelbex  10007  indstr2  10018  ublbneg  10022  irraddap  10056  irrmulap  10058  elpq  10059  elpqb  10060  elrp  10066  mnfltxr  10198  nn0pnfge0  10203  xrltnsym  10205  xrlttr  10207  xrltso  10208  xrlttri3  10209  xrltne  10225  ngtmnft  10229  nmnfgt  10230  xrrebnd  10231  z2ge  10238  xltnegi  10247  xltadd1  10288  xsubge0  10293  xleaddadd  10299  ixxval  10308  elixx1  10309  elioo2  10333  iccid  10337  iccsupr  10378  repos  10382  fzval  10423  elfz1  10426  fzm1  10517  zsupcllemstep  10672  suprzubdc  10681  zsupssdc  10683  qdclt  10690  exbtwnzlemstep  10692  exbtwnzlemex  10694  qbtwnre  10701  qbtwnxr  10702  flval  10717  apbtwnz  10719  modqid2  10801  modqmuladdnn0  10818  exp3val  10991  expge0  11025  expge1  11026  nn0ltexp2  11161  facdiv  11190  facwordi  11192  hashinfom  11231  hashennn  11233  hashunlem  11258  zfz1iso  11307  wrdlen1  11356  fstwrdne0  11358  wrdl1exs1  11411  pfxsuffeqwrdeq  11484  pfxsuff1eqwrdeq  11485  ccats1pfxeq  11500  ccats1pfxeqrex  11501  pfxccatin12lem3  11518  ovshftex  11598  shftfibg  11599  shftfib  11602  shftfn  11603  2shfti  11610  sqrt0rlem  11783  resqrexlemex  11805  rsqrmo  11807  resqrtcl  11809  rersqrtthlem  11810  sqrtsq  11824  cau3lem  11895  caubnd2  11898  maxleim  11986  maxabslemval  11989  maxleast  11994  maxleb  11997  fimaxre2  12008  minmax  12011  xrmaxleim  12026  xrmaxiflemval  12032  xrmaxaddlem  12042  xrminmax  12047  xrbdtri  12058  climi  12069  climeu  12078  climmo  12080  2clim  12083  addcn2  12092  mulcn2  12094  reccn2ap  12095  cn1lem  12096  summodc  12166  zsumdc  12167  fsum3  12170  cvgratz  12315  ntrivcvgap0  12332  prodmodc  12361  zproddc  12362  fprodseq  12366  fprodntrivap  12367  sinltxirr  12544  dvdsabsb  12593  0dvds  12594  alzdvds  12637  dvdsext  12638  fzo0dvdseq  12640  2tp1odd  12667  2teven  12670  divalglemnn  12701  divalglemeunn  12704  divalglemeuneg  12706  bitsinv1lem  12744  gcdval  12752  gcddvds  12756  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemex  12794  bezoutlemeu  12800  bezoutlemsup  12802  dfgcd3  12803  bezout  12804  dvdsgcd  12805  dfgcd2  12807  dvdssq  12824  uzwodc  12830  nnwofdc  12831  lcmval  12857  lcmcllem  12861  dvdslcm  12863  lcmledvds  12864  lcmgcdlem  12871  lcmdvds  12873  coprmgcdb  12882  coprmdvds2  12887  cncongr1  12897  cncongr2  12898  isprm  12903  dvdsnprmd  12919  dvdsprm  12932  exprmfct  12933  isprm6  12942  prmexpb  12946  prmfac1  12947  rpexp  12948  sqrt2irr  12957  nnmaxpwlemparts  12968  nnmaxpw  12969  sqpweven  12971  2sqpwodd  12972  sqne2sq  12973  nnoddn2prmb  13061  pceu  13094  pczpre  13096  pcdiv  13101  pcdvdsb  13119  difsqpwdvds  13137  pcmpt  13142  pcmptdvds  13144  oddprmdvds  13153  prmpwdvds  13154  infpnlem2  13159  ballotfilemfcc  13282  oddennn  13332  evenennn  13333  exmidunben  13366  nninfdclemcl  13388  nninfdclemp1  13390  nninfdc  13393  infpn2  13396  eqgen  14079  zndvds  15033  znleval  15037  comet  15649  metcnpi  15665  metcnpi2  15666  metcnpi3  15667  addcncntoplem  15711  cncfi  15728  elcncf1di  15729  mulcncflem  15757  dedekindeulemuub  15767  dedekindeulemloc  15769  dedekindeulemlu  15771  dedekindeulemeu  15772  dedekindeu  15773  suplociccreex  15774  suplociccex  15775  dedekindicclemuub  15776  dedekindicclemloc  15778  dedekindicclemlu  15780  dedekindicclemeu  15781  dedekindicclemicc  15782  dedekindicc  15783  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemloc  15791  ivthinc  15793  ivthreinc  15795  dich0  15802  ivthdich  15803  limcimo  15815  cnplimclemr  15819  limccnp2lem  15826  limccoap  15828  eldvap  15832  logltb  16026  zprmlogbaplem3  16136  zprmlogbap  16137  pellexlem3  16150  ppiublem1  16192  bpos1lem  16207  lgsdir  16252  lgsne0  16255  gausslemma2dlem0i  16274  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  2lgslem2  16309  2lgs  16321  2sqlem6  16337  2sqlem8  16340  2sqlem10  16342  lfgredg2dom  16471  istrl  16724  clwwlkn0  16747  clwwlkext2edg  16761  clwwlknonccat  16772  clwwlknonex2  16778  iseupth  16786  konigsberg  16832  lealltlt2  16850  sbthom  17169  trilpo  17190  trirec0  17191  apdiff  17195  reap0  17206  cndcap  17207  nconstwlpolem  17213  neapmkv  17216  neap0mkv  17217  ltlenmkv  17218