Theorem breq2d 4137

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
breq2d	⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Proof of Theorem breq2d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq2 4129	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   class class class wbr 4125

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 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 theorem 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 3711  df-pr 3712  df-op 3714  df-br 4126

This theorem is referenced by:  breqtrd  4151  sbcbr1g  4182  pofun  4452  csbfv12g  5730  isorel  6004  isocnv  6007  isotr  6012  caovordig  6245  caovordg  6247  caovord  6251  xporderlem  6457  th3qlem2  6902  phplem3g  7147  supsnti  7335  inflbti  7354  difinfinf  7431  enqdc1  7719  ltanqg  7757  ltmnqg  7758  archnqq  7774  prarloclemarch2  7776  prloc  7848  addnqprllem  7884  addlocprlemgt  7891  appdivnq  7920  mulnqprl  7925  1idprl  7947  ltexprlemloc  7964  caucvgprlemcanl  8001  cauappcvgprlemm  8002  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlemlim  8018  cauappcvgpr  8019  archrecnq  8020  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemcl  8033  caucvgprlemladdrl  8035  caucvgpr  8039  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemnkeqj  8047  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlemclphr  8062  caucvgprprlemexbt  8063  caucvgprprlem1  8066  caucvgprprlem2  8067  caucvgprpr  8069  ltposr  8120  ltasrg  8127  mulgt0sr  8135  mulextsr1lem  8137  mulextsr1  8138  prsrlt  8144  caucvgsrlemcl  8146  caucvgsrlemfv  8148  caucvgsrlembound  8151  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  caucvgsr  8159  map2psrprg  8162  pitonnlem2  8204  pitonn  8205  recidpipr  8213  axpre-ltadd  8243  axpre-mulgt0  8244  axpre-mulext  8245  axarch  8248  nntopi  8251  axcaucvglemval  8254  axcaucvglemcau  8255  axcaucvglemres  8256  axpre-suploclemres  8258  ltaddneg  8742  ltsubadd2  8751  lesubadd2  8753  ltaddsub  8754  leaddsub  8756  ltaddpos2  8771  posdif  8773  lesub1  8774  ltsub1  8776  ltnegcon1  8781  lenegcon1  8784  addge02  8791  leaddle0  8795  ltordlem  8800  possumd  8887  sublt0d  8888  apreap  8905  prodgt02  9173  prodge02  9175  ltmulgt12  9185  lemulge12  9187  ltdivmul  9196  ledivmul  9197  ltdivmul2  9198  lt2mul2div  9199  ledivmul2  9200  ltrec  9203  ltrec1  9208  ltdiv23  9212  lediv23  9213  nnge1  9306  halfpos  9515  lt2halves  9520  addltmul  9521  avglt2  9524  avgle2  9526  nnrecl  9540  zltlem1  9681  difgtsumgt  9693  nn0le2is012  9707  gtndiv  9720  qapne  10018  nnledivrp  10146  xltnegi  10216  xltadd1  10257  xsubge0  10262  xposdif  10263  xlesubadd  10264  xleaddadd  10268  divelunit  10383  eluzgtdifelfzo  10593  qtri3or  10653  exbtwnzlemstep  10660  exbtwnzlemshrink  10661  exbtwnzlemex  10662  exbtwnz  10663  rebtwn2zlemstep  10665  rebtwn2zlemshrink  10666  rebtwn2z  10667  flqlelt  10689  flqbi  10703  2tnp1ge0ge0  10714  q2submod  10800  frec2uzltd  10818  frec2uzlt2d  10819  frec2uzf1od  10821  monoord  10900  ser3mono  10902  ser3ge0  10951  expnbnd  11079  nn0ltexp2  11125  facwordi  11156  hashunlem  11222  ssenneg  11258  zfz1isolemiso  11269  seq3coll  11272  swrdccat3blem  11489  caucvgrelemcau  11724  caucvgre  11725  cvg1nlemcau  11728  cvg1nlemres  11729  recvguniq  11739  resqrexlemover  11754  resqrexlemgt0  11764  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemsqa  11768  resqrexlemex  11769  maxleastlt  11959  minmax  11974  lemininf  11978  ltmininf  11979  xrmaxleastlt  12000  xrmaxltsup  12002  xrminmax  12009  xrmin1inf  12011  xrmin2inf  12012  xrltmininf  12014  xrlemininf  12015  climserle  12089  summodclem3  12125  summodclem2a  12126  summodc  12128  zsumdc  12129  fsum3  12132  fsum00  12207  fsumabs  12210  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  zproddc  12324  fprodseq  12328  fprodle  12385  sin01bnd  12502  cos01bnd  12503  summodnegmod  12567  modmulconst  12568  dvdsaddr  12582  dvdssub  12583  dvdssubr  12584  dvdslelemd  12588  dvdsfac  12605  dvdsmod  12607  oddp1even  12621  ltoddhalfle  12638  opoe  12640  omoe  12641  divalg2  12671  divalgmod  12672  ndvdssub  12675  ndvdsadd  12676  bitsfval  12687  bitsval  12688  bits0  12693  bitsp1  12696  bitsfzolem  12699  bitsfzo  12700  bitscmp  12703  bitsinv1lem  12706  bezoutlembi  12760  dvdssqim  12779  dvdsmulgcd  12780  dvdssq  12786  nn0seqcvgd  12797  coprmdvds  12848  coprmdvds2  12849  rpmul  12854  cncongr1  12859  divgcdodd  12899  isprm6  12903  prmdvdsexp  12904  prmdvdsexpr  12906  prmfac1  12908  oddpwdclemxy  12925  oddpwdclemodd  12928  sqpweven  12931  2sqpwodd  12932  sqne2sq  12933  hashdvds  12977  phiprmpw  12978  eulerthlemh  12987  prmdiv  12991  prmdiveq  12992  odzval  12998  odzcllem  12999  odzdvds  13002  pythagtriplem11  13031  pythagtriplem13  13033  pythagtrip  13040  pceulem  13051  pczndvds2  13075  pcdvdsb  13077  pc2dvds  13087  pcz  13089  pcprmpw2  13090  dvdsprmpweq  13092  dvdsprmpweqle  13094  difsqpwdvds  13095  pcmpt  13100  prmpwdvds  13112  pockthlem  13113  4sqlem11  13158  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfileme  13214  ballotfilemefi  13215  ballotfilemodife  13218  ballotfilem4  13219  ballotfilem1c  13229  ballotfilemsval  13230  ballotfilemieq  13238  ballotfilemfrcn0  13251  ballotfi  13260  exmidunben  13295  nninfdclemlt  13320  mulgval  13902  dvdsrtr  14381  dvdsrmul1  14382  unitnegcl  14410  unitpropdg  14428  elrhmunit  14457  zndvds0  14957  znunit  14966  mplsubgfilemcl  15013  psmettri2  15352  ismet2  15378  xmettri2  15385  comet  15523  ivthinclemum  15659  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemdisj  15664  ivthinclemloc  15665  ivthinc  15667  ivthreinc  15669  limccl  15683  ellimc3apf  15684  sin0pilem2  15806  pilem3  15807  sincosq1sgn  15850  sincosq2sgn  15851  sincosq4sgn  15853  logltb  15898  logle1b  15916  loglt1b  15917  logbgt0b  15991  wilthlem1  16008  sgmval  16011  dvdsppwf1o  16017  perfect1  16026  lgslem1  16033  lgsval  16037  lgsdilem  16060  lgsne0  16071  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  lgseisenlem1  16103  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem2  16115  m1lgs  16118  2lgslem1a1  16119  2lgslem1a  16121  2lgsoddprmlem2  16139  2lgsoddprmlem3  16144  2sqlem4  16151  2sqlem8a  16155  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  eupth2lem3lem7fi  16629  eupth2lemsfi  16633  eupth2fi  16634  konigsberglem4  16646