Theorem breq2 4048

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2176  ⟨cop 3636   class class class wbr 4044

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045

This theorem is referenced by:  breq12  4049  breq2i  4052  breq2d  4056  nbrne1  4063  brralrspcev  4102  brimralrspcev  4103  pocl  4350  swopolem  4352  swopo  4353  sowlin  4367  sotricim  4370  sotritrieq  4372  seex  4382  frind  4399  wetriext  4625  vtoclr  4723  posng  4747  brcog  4845  brcogw  4847  opelcnvg  4858  dfdmf  4871  breldmg  4884  dfrnf  4919  dmcoss  4948  resieq  4969  dfres2  5011  elimag  5026  elrelimasn  5048  elimasn  5049  intirr  5069  poirr2  5075  poltletr  5083  dffun6f  5284  dffun4f  5287  fun11  5341  brprcneu  5569  fv3  5599  tz6.12c  5606  relelfvdm  5608  funbrfv  5617  fnbrfvb  5619  funfvdm2f  5644  fndmdif  5685  dff3im  5725  fmptco  5746  foeqcnvco  5859  isorel  5877  isocnv  5880  isotr  5885  isopolem  5891  isosolem  5893  f1oiso  5895  f1oiso2  5896  caovordig  6112  caovordg  6114  caovord  6118  caofrss  6190  caoftrn  6191  poxp  6318  tposoprab  6366  ertr  6635  ecopovsym  6718  ecopovtrn  6719  ecopovsymg  6721  ecopovtrng  6722  th3qlem2  6725  domeng  6841  eqeng  6857  snfig  6906  nneneq  6954  nnfi  6969  ssfilem  6972  domfiexmid  6975  dif1enen  6977  diffitest  6984  findcard  6985  findcard2  6986  findcard2s  6987  diffisn  6990  tridc  6996  fimax2gtrilemstep  6997  inffiexmid  7003  unsnfi  7016  fiintim  7028  fisseneq  7031  isbth  7069  supmoti  7095  eqsupti  7098  supubti  7101  suplubti  7102  suplub2ti  7103  supmaxti  7106  supsnti  7107  isotilem  7108  isoti  7109  supisolem  7110  supisoex  7111  cardcl  7288  isnumi  7289  cardval3ex  7292  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidapne  7372  nqtri3or  7509  ltsonq  7511  ltanqg  7513  ltmnqg  7514  ltexnqq  7521  nsmallnqq  7525  subhalfnqq  7527  ltbtwnnqq  7528  prarloclemarch2  7532  nqnq0pi  7551  prcdnql  7597  prcunqu  7598  prnminu  7602  genpcdl  7632  genprndl  7634  genprndu  7635  genpdisj  7636  nqprm  7655  nqprrnd  7656  nqprdisj  7657  nqprloc  7658  nqprlu  7660  nqprl  7664  addnqprlemru  7671  addnqprlemfl  7672  addnqprlemfu  7673  mulnqprlemru  7687  mulnqprlemfl  7688  mulnqprlemfu  7689  1idpru  7704  ltnqpr  7706  ltnqpri  7707  prplnqu  7733  recexprlemelu  7736  recexprlemm  7737  recexprlemloc  7744  recexprlem1ssl  7746  recexprlemss1u  7749  cauappcvgprlemm  7758  cauappcvgprlemopu  7761  cauappcvgprlemupu  7762  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdfu  7767  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem2  7773  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemopu  7784  caucvgprlemupu  7785  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem2  7793  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnbj  7806  caucvgprprlemmu  7808  caucvgprprlemexbt  7819  caucvgprprlemaddq  7821  caucvgprprlem1  7822  caucvgprprlem2  7823  suplocexprlemmu  7831  suplocexprlemru  7832  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemub  7836  suplocexpr  7838  lttrsr  7875  ltsosr  7877  ltasrg  7883  recexgt0sr  7886  mulgt0sr  7891  aptisr  7892  mulextsr1  7894  srpospr  7896  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  caucvgsr  7915  map2psrprg  7918  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  axprecex  7993  axpre-ltwlin  7996  axpre-lttrn  7997  axpre-apti  7998  axpre-ltadd  7999  axpre-mulgt0  8000  axpre-mulext  8001  axcaucvglemcau  8011  axcaucvglemres  8012  axcaucvg  8013  axpre-suploclemres  8014  axpre-suploc  8015  ltxrlt  8138  lttri3  8152  ltne  8157  eqle  8164  ltordlem  8555  reapti  8652  apreim  8676  squeeze0  8977  lbreu  9018  lble  9020  suprleubex  9027  sup3exmid  9030  nnge1  9059  nn2ge  9069  nn1gt1  9070  nnsub  9075  nominpos  9275  nn0ge0  9320  elnnnn0b  9339  nn0ge2m1nn  9355  zdclt  9450  suprzclex  9471  peano2uz2  9480  peano5uzti  9481  dfuzi  9483  uzind  9484  uzind3  9486  eluz1  9652  uzind4  9709  indstr  9714  supinfneg  9716  infsupneg  9717  infregelbex  9719  indstr2  9730  ublbneg  9734  irrmulap  9769  elpq  9770  elpqb  9771  elrp  9777  mnfltxr  9908  nn0pnfge0  9913  xrltnsym  9915  xrlttr  9917  xrltso  9918  xrlttri3  9919  xrltne  9935  ngtmnft  9939  nmnfgt  9940  xrrebnd  9941  z2ge  9948  xltnegi  9957  xltadd1  9998  xsubge0  10003  xleaddadd  10009  ixxval  10018  elixx1  10019  elioo2  10043  iccid  10047  iccsupr  10088  repos  10092  fzval  10132  elfz1  10135  fzm1  10222  zsupcllemstep  10372  suprzubdc  10379  zsupssdc  10381  qdclt  10388  exbtwnzlemstep  10390  exbtwnzlemex  10392  qbtwnre  10399  qbtwnxr  10400  flval  10415  apbtwnz  10417  modqid2  10496  modqmuladdnn0  10513  exp3val  10686  expge0  10720  expge1  10721  nn0ltexp2  10854  facdiv  10883  facwordi  10885  hashinfom  10923  hashennn  10925  hashunlem  10949  zfz1iso  10986  wrdlen1  11031  fstwrdne0  11033  wrdl1exs1  11083  ovshftex  11130  shftfibg  11131  shftfib  11134  shftfn  11135  2shfti  11142  sqrt0rlem  11314  resqrexlemex  11336  rsqrmo  11338  resqrtcl  11340  rersqrtthlem  11341  sqrtsq  11355  cau3lem  11425  caubnd2  11428  maxleim  11516  maxabslemval  11519  maxleast  11524  maxleb  11527  fimaxre2  11538  minmax  11541  xrmaxleim  11555  xrmaxiflemval  11561  xrmaxaddlem  11571  xrminmax  11576  xrbdtri  11587  climi  11598  climeu  11607  climmo  11609  2clim  11612  addcn2  11621  mulcn2  11623  reccn2ap  11624  cn1lem  11625  summodc  11694  zsumdc  11695  fsum3  11698  cvgratz  11843  ntrivcvgap0  11860  prodmodc  11889  zproddc  11890  fprodseq  11894  fprodntrivap  11895  sinltxirr  12072  dvdsabsb  12121  0dvds  12122  alzdvds  12165  dvdsext  12166  fzo0dvdseq  12168  2tp1odd  12195  2teven  12198  divalglemnn  12229  divalglemeunn  12232  divalglemeuneg  12234  bitsinv1lem  12272  gcdval  12280  gcddvds  12284  bezoutlemstep  12318  bezoutlemmain  12319  bezoutlemex  12322  bezoutlemeu  12328  bezoutlemsup  12330  dfgcd3  12331  bezout  12332  dvdsgcd  12333  dfgcd2  12335  dvdssq  12352  uzwodc  12358  nnwofdc  12359  lcmval  12385  lcmcllem  12389  dvdslcm  12391  lcmledvds  12392  lcmgcdlem  12399  lcmdvds  12401  coprmgcdb  12410  coprmdvds2  12415  cncongr1  12425  cncongr2  12426  isprm  12431  dvdsnprmd  12447  dvdsprm  12459  exprmfct  12460  isprm6  12469  prmexpb  12473  prmfac1  12474  rpexp  12475  sqrt2irr  12484  oddpwdclemdc  12495  oddpwdc  12496  sqpweven  12497  2sqpwodd  12498  sqne2sq  12499  nnoddn2prmb  12585  pceu  12618  pczpre  12620  pcdiv  12625  pcdvdsb  12643  difsqpwdvds  12661  pcmpt  12666  pcmptdvds  12668  oddprmdvds  12677  prmpwdvds  12678  infpnlem2  12683  oddennn  12763  evenennn  12764  exmidunben  12797  nninfdclemcl  12819  nninfdclemp1  12821  nninfdc  12824  infpn2  12827  eqgen  13563  zndvds  14411  znleval  14415  comet  14971  metcnpi  14987  metcnpi2  14988  metcnpi3  14989  addcncntoplem  15033  cncfi  15050  elcncf1di  15051  mulcncflem  15079  dedekindeulemuub  15089  dedekindeulemloc  15091  dedekindeulemlu  15093  dedekindeulemeu  15094  dedekindeu  15095  suplociccreex  15096  suplociccex  15097  dedekindicclemuub  15098  dedekindicclemloc  15100  dedekindicclemlu  15102  dedekindicclemeu  15103  dedekindicclemicc  15104  dedekindicc  15105  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemloc  15113  ivthinc  15115  ivthreinc  15117  dich0  15124  ivthdich  15125  limcimo  15137  cnplimclemr  15141  limccnp2lem  15148  limccoap  15150  eldvap  15154  logltb  15346  lgsdir  15512  lgsne0  15515  gausslemma2dlem0i  15534  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  2lgslem2  15569  2lgs  15581  2sqlem6  15597  2sqlem8  15600  2sqlem10  15602  sbthom  15965  trilpo  15982  trirec0  15983  apdiff  15987  reap0  15997  cndcap  15998  nconstwlpolem  16004  neapmkv  16007  neap0mkv  16008  ltlenmkv  16009