Theorem breq2 4090

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 3861	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	eleq1d 2298	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3		df-br 4087	. 2 ⊢ (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4		df-br 4087	. 2 ⊢ (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ⟨cop 3670   class class class wbr 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  breq12  4091  breq2i  4094  breq2d  4098  nbrne1  4105  brralrspcev  4145  brimralrspcev  4146  pocl  4398  swopolem  4400  swopo  4401  sowlin  4415  sotricim  4418  sotritrieq  4420  seex  4430  frind  4447  wetriext  4673  vtoclr  4772  posng  4796  brcog  4895  brcogw  4897  opelcnvg  4908  dfdmf  4922  breldmg  4935  dfrnf  4971  dmcoss  5000  resieq  5021  dfres2  5063  elimag  5078  elrelimasn  5100  elimasn  5101  intirr  5121  poirr2  5127  poltletr  5135  dffun6f  5337  dffun4f  5340  fun11  5394  brprcneu  5628  fv3  5658  tz6.12c  5665  relelfvdm  5667  fvmbr  5670  funbrfv  5678  fnbrfvb  5680  funfvdm2f  5707  fndmdif  5748  dff3im  5788  fmptco  5809  foeqcnvco  5926  isorel  5944  isocnv  5947  isotr  5952  isopolem  5958  isosolem  5960  f1oiso  5962  f1oiso2  5963  caovordig  6183  caovordg  6185  caovord  6189  caofrss  6262  caoftrn  6263  poxp  6392  tposoprab  6441  ertr  6712  ecopovsym  6795  ecopovtrn  6796  ecopovsymg  6798  ecopovtrng  6799  th3qlem2  6802  domeng  6918  eqeng  6934  snfig  6984  nneneq  7038  nnfi  7054  ssfilem  7057  domfiexmid  7060  dif1enen  7062  diffitest  7069  findcard  7070  findcard2  7071  findcard2s  7072  diffisn  7075  tridc  7082  fimax2gtrilemstep  7083  inffiexmid  7091  unsnfi  7104  fiintim  7116  fisseneq  7119  isbth  7157  supmoti  7183  eqsupti  7186  supubti  7189  suplubti  7190  suplub2ti  7191  supmaxti  7194  supsnti  7195  isotilem  7196  isoti  7197  supisolem  7198  supisoex  7199  cardcl  7376  isnumi  7377  cardval3ex  7380  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidapne  7469  nqtri3or  7606  ltsonq  7608  ltanqg  7610  ltmnqg  7611  ltexnqq  7618  nsmallnqq  7622  subhalfnqq  7624  ltbtwnnqq  7625  prarloclemarch2  7629  nqnq0pi  7648  prcdnql  7694  prcunqu  7695  prnminu  7699  genpcdl  7729  genprndl  7731  genprndu  7732  genpdisj  7733  nqprm  7752  nqprrnd  7753  nqprdisj  7754  nqprloc  7755  nqprlu  7757  nqprl  7761  addnqprlemru  7768  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprlemru  7784  mulnqprlemfl  7785  mulnqprlemfu  7786  1idpru  7801  ltnqpr  7803  ltnqpri  7804  prplnqu  7830  recexprlemelu  7833  recexprlemm  7834  recexprlemloc  7841  recexprlem1ssl  7843  recexprlemss1u  7846  cauappcvgprlemm  7855  cauappcvgprlemopu  7858  cauappcvgprlemupu  7859  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfu  7864  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem2  7870  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemopu  7881  caucvgprlemupu  7882  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem2  7890  caucvgprprlemelu  7896  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnbj  7903  caucvgprprlemmu  7905  caucvgprprlemexbt  7916  caucvgprprlemaddq  7918  caucvgprprlem1  7919  caucvgprprlem2  7920  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  suplocexpr  7935  lttrsr  7972  ltsosr  7974  ltasrg  7980  recexgt0sr  7983  mulgt0sr  7988  aptisr  7989  mulextsr1  7991  srpospr  7993  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  caucvgsr  8012  map2psrprg  8015  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  axprecex  8090  axpre-ltwlin  8093  axpre-lttrn  8094  axpre-apti  8095  axpre-ltadd  8096  axpre-mulgt0  8097  axpre-mulext  8098  axcaucvglemcau  8108  axcaucvglemres  8109  axcaucvg  8110  axpre-suploclemres  8111  axpre-suploc  8112  ltxrlt  8235  lttri3  8249  ltne  8254  eqle  8261  ltordlem  8652  reapti  8749  apreim  8773  squeeze0  9074  lbreu  9115  lble  9117  suprleubex  9124  sup3exmid  9127  nnge1  9156  nn2ge  9166  nn1gt1  9167  nnsub  9172  nominpos  9372  nn0ge0  9417  elnnnn0b  9436  nn0ge2m1nn  9452  zdclt  9547  suprzclex  9568  peano2uz2  9577  peano5uzti  9578  dfuzi  9580  uzind  9581  uzind3  9583  eluz1  9749  uzind4  9812  indstr  9817  supinfneg  9819  infsupneg  9820  infregelbex  9822  indstr2  9833  ublbneg  9837  irrmulap  9872  elpq  9873  elpqb  9874  elrp  9880  mnfltxr  10011  nn0pnfge0  10016  xrltnsym  10018  xrlttr  10020  xrltso  10021  xrlttri3  10022  xrltne  10038  ngtmnft  10042  nmnfgt  10043  xrrebnd  10044  z2ge  10051  xltnegi  10060  xltadd1  10101  xsubge0  10106  xleaddadd  10112  ixxval  10121  elixx1  10122  elioo2  10146  iccid  10150  iccsupr  10191  repos  10195  fzval  10235  elfz1  10238  fzm1  10325  zsupcllemstep  10479  suprzubdc  10486  zsupssdc  10488  qdclt  10495  exbtwnzlemstep  10497  exbtwnzlemex  10499  qbtwnre  10506  qbtwnxr  10507  flval  10522  apbtwnz  10524  modqid2  10603  modqmuladdnn0  10620  exp3val  10793  expge0  10827  expge1  10828  nn0ltexp2  10961  facdiv  10990  facwordi  10992  hashinfom  11030  hashennn  11032  hashunlem  11057  zfz1iso  11095  wrdlen1  11141  fstwrdne0  11143  wrdl1exs1  11196  pfxsuffeqwrdeq  11269  pfxsuff1eqwrdeq  11270  ccats1pfxeq  11285  ccats1pfxeqrex  11286  pfxccatin12lem3  11303  ovshftex  11370  shftfibg  11371  shftfib  11374  shftfn  11375  2shfti  11382  sqrt0rlem  11554  resqrexlemex  11576  rsqrmo  11578  resqrtcl  11580  rersqrtthlem  11581  sqrtsq  11595  cau3lem  11665  caubnd2  11668  maxleim  11756  maxabslemval  11759  maxleast  11764  maxleb  11767  fimaxre2  11778  minmax  11781  xrmaxleim  11795  xrmaxiflemval  11801  xrmaxaddlem  11811  xrminmax  11816  xrbdtri  11827  climi  11838  climeu  11847  climmo  11849  2clim  11852  addcn2  11861  mulcn2  11863  reccn2ap  11864  cn1lem  11865  summodc  11934  zsumdc  11935  fsum3  11938  cvgratz  12083  ntrivcvgap0  12100  prodmodc  12129  zproddc  12130  fprodseq  12134  fprodntrivap  12135  sinltxirr  12312  dvdsabsb  12361  0dvds  12362  alzdvds  12405  dvdsext  12406  fzo0dvdseq  12408  2tp1odd  12435  2teven  12438  divalglemnn  12469  divalglemeunn  12472  divalglemeuneg  12474  bitsinv1lem  12512  gcdval  12520  gcddvds  12524  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlemex  12562  bezoutlemeu  12568  bezoutlemsup  12570  dfgcd3  12571  bezout  12572  dvdsgcd  12573  dfgcd2  12575  dvdssq  12592  uzwodc  12598  nnwofdc  12599  lcmval  12625  lcmcllem  12629  dvdslcm  12631  lcmledvds  12632  lcmgcdlem  12639  lcmdvds  12641  coprmgcdb  12650  coprmdvds2  12655  cncongr1  12665  cncongr2  12666  isprm  12671  dvdsnprmd  12687  dvdsprm  12699  exprmfct  12700  isprm6  12709  prmexpb  12713  prmfac1  12714  rpexp  12715  sqrt2irr  12724  oddpwdclemdc  12735  oddpwdc  12736  sqpweven  12737  2sqpwodd  12738  sqne2sq  12739  nnoddn2prmb  12825  pceu  12858  pczpre  12860  pcdiv  12865  pcdvdsb  12883  difsqpwdvds  12901  pcmpt  12906  pcmptdvds  12908  oddprmdvds  12917  prmpwdvds  12918  infpnlem2  12923  oddennn  13003  evenennn  13004  exmidunben  13037  nninfdclemcl  13059  nninfdclemp1  13061  nninfdc  13064  infpn2  13067  eqgen  13804  zndvds  14653  znleval  14657  comet  15213  metcnpi  15229  metcnpi2  15230  metcnpi3  15231  addcncntoplem  15275  cncfi  15292  elcncf1di  15293  mulcncflem  15321  dedekindeulemuub  15331  dedekindeulemloc  15333  dedekindeulemlu  15335  dedekindeulemeu  15336  dedekindeu  15337  suplociccreex  15338  suplociccex  15339  dedekindicclemuub  15340  dedekindicclemloc  15342  dedekindicclemlu  15344  dedekindicclemeu  15345  dedekindicclemicc  15346  dedekindicc  15347  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemloc  15355  ivthinc  15357  ivthreinc  15359  dich0  15366  ivthdich  15367  limcimo  15379  cnplimclemr  15383  limccnp2lem  15390  limccoap  15392  eldvap  15396  logltb  15588  lgsdir  15754  lgsne0  15757  gausslemma2dlem0i  15776  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  2lgslem2  15811  2lgs  15823  2sqlem6  15839  2sqlem8  15842  2sqlem10  15844  lfgredg2dom  15971  istrl  16180  clwwlkn0  16203  clwwlkext2edg  16217  clwwlknonccat  16228  clwwlknonex2  16234  iseupth  16242  sbthom  16566  trilpo  16583  trirec0  16584  apdiff  16588  reap0  16598  cndcap  16599  nconstwlpolem  16605  neapmkv  16608  neap0mkv  16609  ltlenmkv  16610