Theorem breq2 4113

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2203  ⟨cop 3692   class class class wbr 4109

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110

This theorem is referenced by:  breq12  4114  breq2i  4117  breq2d  4121  nbrne1  4128  brralrspcev  4168  brimralrspcev  4169  pocl  4424  swopolem  4426  swopo  4427  sowlin  4441  sotricim  4444  sotritrieq  4446  seex  4456  frind  4473  wetriext  4699  vtoclr  4798  posng  4822  brcog  4922  brcogw  4924  opelcnvg  4935  dfdmf  4949  breldmg  4962  dfrnf  4998  dmcoss  5027  resieq  5048  dfres2  5090  elimag  5105  elrelimasn  5128  elimasn  5129  intirr  5149  poirr2  5155  poltletr  5163  dffun6f  5365  dffun4f  5368  fun11  5423  brprcneu  5663  fv3  5693  tz6.12c  5700  relelfvdm  5702  fvmbr  5705  funbrfv  5713  fnbrfvb  5715  funfvdm2f  5742  fndmdif  5783  dff3im  5822  fmptco  5843  foeqcnvco  5963  isorel  5981  isocnv  5984  isotr  5989  isopolem  5995  isosolem  5997  f1oiso  5999  f1oiso2  6000  caovordig  6220  caovordg  6222  caovord  6226  caofrss  6298  caoftrn  6299  poxp  6428  tposoprab  6511  ertr  6782  ecopovsym  6865  ecopovtrn  6866  ecopovsymg  6868  ecopovtrng  6869  th3qlem2  6872  domeng  6989  eqeng  7005  snfig  7056  nneneq  7111  nnfi  7127  ssfilem  7130  ssfilemd  7132  domfiexmid  7135  dif1enen  7137  diffitest  7144  findcard  7145  findcard2  7146  findcard2s  7147  diffisn  7150  tridc  7157  fimax2gtrilemstep  7158  inffiexmid  7166  unsnfi  7179  fiintim  7191  fisseneq  7195  isbth  7237  supmoti  7284  eqsupti  7287  supubti  7290  suplubti  7291  suplub2ti  7292  supmaxti  7295  supsnti  7296  isotilem  7297  isoti  7298  supisolem  7299  supisoex  7300  cardcl  7477  isnumi  7478  cardval3ex  7481  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  papsym  7561  papcotr  7562  exmidapne  7574  nqtri3or  7711  ltsonq  7713  ltanqg  7715  ltmnqg  7716  ltexnqq  7723  nsmallnqq  7727  subhalfnqq  7729  ltbtwnnqq  7730  prarloclemarch2  7734  nqnq0pi  7753  prcdnql  7799  prcunqu  7800  prnminu  7804  genpcdl  7834  genprndl  7836  genprndu  7837  genpdisj  7838  nqprm  7857  nqprrnd  7858  nqprdisj  7859  nqprloc  7860  nqprlu  7862  nqprl  7866  addnqprlemru  7873  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprlemru  7889  mulnqprlemfl  7890  mulnqprlemfu  7891  1idpru  7906  ltnqpr  7908  ltnqpri  7909  prplnqu  7935  recexprlemelu  7938  recexprlemm  7939  recexprlemloc  7946  recexprlem1ssl  7948  recexprlemss1u  7951  cauappcvgprlemm  7960  cauappcvgprlemopu  7963  cauappcvgprlemupu  7964  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdfu  7969  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem2  7975  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemopu  7986  caucvgprlemupu  7987  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem2  7995  caucvgprprlemelu  8001  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemnbj  8008  caucvgprprlemmu  8010  caucvgprprlemexbt  8021  caucvgprprlemaddq  8023  caucvgprprlem1  8024  caucvgprprlem2  8025  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemub  8038  suplocexpr  8040  lttrsr  8077  ltsosr  8079  ltasrg  8085  recexgt0sr  8088  mulgt0sr  8093  aptisr  8094  mulextsr1  8096  srpospr  8098  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  caucvgsr  8117  map2psrprg  8120  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  axprecex  8195  axpre-ltwlin  8198  axpre-lttrn  8199  axpre-apti  8200  axpre-ltadd  8201  axpre-mulgt0  8202  axpre-mulext  8203  axcaucvglemcau  8213  axcaucvglemres  8214  axcaucvg  8215  axpre-suploclemres  8216  axpre-suploc  8217  ltxrlt  8339  lttri3  8353  ltne  8358  eqle  8365  ltordlem  8756  reapti  8853  apreim  8877  squeeze0  9178  lbreu  9219  lble  9221  suprleubex  9228  sup3exmid  9231  nnge1  9260  nn2ge  9270  nn1gt1  9271  nnsub  9276  nominpos  9476  nn0ge0  9521  elnnnn0b  9540  nn0ge2m1nn  9560  zdclt  9655  suprzclex  9676  peano2uz2  9685  peano5uzti  9686  dfuzi  9688  uzind  9689  uzind3  9691  eluz1  9857  uzind4  9920  indstr  9925  supinfneg  9927  infsupneg  9928  infregelbex  9930  indstr2  9941  ublbneg  9945  irrmulap  9980  elpq  9981  elpqb  9982  elrp  9988  mnfltxr  10119  nn0pnfge0  10124  xrltnsym  10126  xrlttr  10128  xrltso  10129  xrlttri3  10130  xrltne  10146  ngtmnft  10150  nmnfgt  10151  xrrebnd  10152  z2ge  10159  xltnegi  10168  xltadd1  10209  xsubge0  10214  xleaddadd  10220  ixxval  10229  elixx1  10230  elioo2  10254  iccid  10258  iccsupr  10299  repos  10303  fzval  10344  elfz1  10347  fzm1  10434  zsupcllemstep  10589  suprzubdc  10596  zsupssdc  10598  qdclt  10605  exbtwnzlemstep  10607  exbtwnzlemex  10609  qbtwnre  10616  qbtwnxr  10617  flval  10632  apbtwnz  10634  modqid2  10713  modqmuladdnn0  10730  exp3val  10903  expge0  10937  expge1  10938  nn0ltexp2  11071  facdiv  11100  facwordi  11102  hashinfom  11141  hashennn  11143  hashunlem  11168  zfz1iso  11213  wrdlen1  11262  fstwrdne0  11264  wrdl1exs1  11317  pfxsuffeqwrdeq  11390  pfxsuff1eqwrdeq  11391  ccats1pfxeq  11406  ccats1pfxeqrex  11407  pfxccatin12lem3  11424  ovshftex  11504  shftfibg  11505  shftfib  11508  shftfn  11509  2shfti  11516  sqrt0rlem  11688  resqrexlemex  11710  rsqrmo  11712  resqrtcl  11714  rersqrtthlem  11715  sqrtsq  11729  cau3lem  11799  caubnd2  11802  maxleim  11890  maxabslemval  11893  maxleast  11898  maxleb  11901  fimaxre2  11912  minmax  11915  xrmaxleim  11929  xrmaxiflemval  11935  xrmaxaddlem  11945  xrminmax  11950  xrbdtri  11961  climi  11972  climeu  11981  climmo  11983  2clim  11986  addcn2  11995  mulcn2  11997  reccn2ap  11998  cn1lem  11999  summodc  12069  zsumdc  12070  fsum3  12073  cvgratz  12218  ntrivcvgap0  12235  prodmodc  12264  zproddc  12265  fprodseq  12269  fprodntrivap  12270  sinltxirr  12447  dvdsabsb  12496  0dvds  12497  alzdvds  12540  dvdsext  12541  fzo0dvdseq  12543  2tp1odd  12570  2teven  12573  divalglemnn  12604  divalglemeunn  12607  divalglemeuneg  12609  bitsinv1lem  12647  gcdval  12655  gcddvds  12659  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlemex  12697  bezoutlemeu  12703  bezoutlemsup  12705  dfgcd3  12706  bezout  12707  dvdsgcd  12708  dfgcd2  12710  dvdssq  12727  uzwodc  12733  nnwofdc  12734  lcmval  12760  lcmcllem  12764  dvdslcm  12766  lcmledvds  12767  lcmgcdlem  12774  lcmdvds  12776  coprmgcdb  12785  coprmdvds2  12790  cncongr1  12800  cncongr2  12801  isprm  12806  dvdsnprmd  12822  dvdsprm  12834  exprmfct  12835  isprm6  12844  prmexpb  12848  prmfac1  12849  rpexp  12850  sqrt2irr  12859  oddpwdclemdc  12870  oddpwdc  12871  sqpweven  12872  2sqpwodd  12873  sqne2sq  12874  nnoddn2prmb  12960  pceu  12993  pczpre  12995  pcdiv  13000  pcdvdsb  13018  difsqpwdvds  13036  pcmpt  13041  pcmptdvds  13043  oddprmdvds  13052  prmpwdvds  13053  infpnlem2  13058  oddennn  13143  evenennn  13144  exmidunben  13177  nninfdclemcl  13199  nninfdclemp1  13201  nninfdc  13204  infpn2  13207  eqgen  13944  zndvds  14797  znleval  14801  comet  15364  metcnpi  15380  metcnpi2  15381  metcnpi3  15382  addcncntoplem  15426  cncfi  15443  elcncf1di  15444  mulcncflem  15472  dedekindeulemuub  15482  dedekindeulemloc  15484  dedekindeulemlu  15486  dedekindeulemeu  15487  dedekindeu  15488  suplociccreex  15489  suplociccex  15490  dedekindicclemuub  15491  dedekindicclemloc  15493  dedekindicclemlu  15495  dedekindicclemeu  15496  dedekindicclemicc  15497  dedekindicc  15498  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemloc  15506  ivthinc  15508  ivthreinc  15510  dich0  15517  ivthdich  15518  limcimo  15530  cnplimclemr  15534  limccnp2lem  15541  limccoap  15543  eldvap  15547  logltb  15739  pellexlem3  15847  lgsdir  15908  lgsne0  15911  gausslemma2dlem0i  15930  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  2lgslem2  15965  2lgs  15977  2sqlem6  15993  2sqlem8  15996  2sqlem10  15998  lfgredg2dom  16127  istrl  16380  clwwlkn0  16403  clwwlkext2edg  16417  clwwlknonccat  16428  clwwlknonex2  16434  iseupth  16442  konigsberg  16488  sbthom  16806  trilpo  16827  trirec0  16828  apdiff  16832  reap0  16843  cndcap  16844  trimul0or  16845  nconstwlpolem  16851  neapmkv  16854  neap0mkv  16855  ltlenmkv  16856