Theorem breq2d 4142

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 4134	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   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:  breqtrd  4156  sbcbr1g  4187  pofun  4457  csbfv12g  5736  isorel  6014  isocnv  6017  isotr  6022  caovordig  6255  caovordg  6257  caovord  6261  xporderlem  6467  th3qlem2  6912  phplem3g  7157  supsnti  7345  inflbti  7364  difinfinf  7441  enqdc1  7729  ltanqg  7767  ltmnqg  7768  archnqq  7784  prarloclemarch2  7786  prloc  7858  addnqprllem  7894  addlocprlemgt  7901  appdivnq  7930  mulnqprl  7935  1idprl  7957  ltexprlemloc  7974  caucvgprlemcanl  8011  cauappcvgprlemm  8012  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  archrecnq  8030  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemcl  8043  caucvgprlemladdrl  8045  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgprpr  8079  ltposr  8130  ltasrg  8137  mulgt0sr  8145  mulextsr1lem  8147  mulextsr1  8148  prsrlt  8154  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsrlembound  8161  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  map2psrprg  8172  pitonnlem2  8214  pitonn  8215  recidpipr  8223  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  axarch  8258  nntopi  8261  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  ltaddneg  8753  ltsubadd2  8762  lesubadd2  8764  ltaddsub  8765  leaddsub  8767  ltaddpos2  8782  posdif  8784  lesub1  8785  ltsub1  8787  ltnegcon1  8792  lenegcon1  8795  addge02  8802  leaddle0  8806  ltordlem  8811  possumd  8899  sublt0d  8900  apreap  8917  prodgt02  9185  prodge02  9187  ltmulgt12  9197  lemulge12  9199  ltdivmul  9208  ledivmul  9209  ltdivmul2  9210  lt2mul2div  9211  ledivmul2  9212  ltrec  9215  ltrec1  9220  ltdiv23  9224  lediv23  9225  nnge1  9329  halfpos  9540  lt2halves  9545  addltmul  9546  avglt2  9549  avgle2  9551  nnrecl  9565  zltlem1  9706  difgtsumgt  9718  nn0le2is012  9732  gtndiv  9745  qapne  10048  nnledivrp  10177  xltnegi  10247  xltadd1  10288  xsubge0  10293  xposdif  10294  xlesubadd  10295  xleaddadd  10299  divelunit  10414  eluzgtdifelfzo  10625  qtri3or  10685  exbtwnzlemstep  10692  exbtwnzlemshrink  10693  exbtwnzlemex  10694  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2zlemshrink  10698  rebtwn2z  10699  flqlelt  10722  flaplelt  10723  flqbi  10738  2tnp1ge0ge0  10749  q2submod  10835  frec2uzltd  10853  frec2uzlt2d  10854  frec2uzf1od  10856  monoord  10935  ser3mono  10937  ser3ge0  10986  expnbnd  11114  nn0ltexp2  11161  facwordi  11192  hashunlem  11258  ssenneg  11294  zfz1isolemiso  11305  seq3coll  11308  swrdccat3blem  11525  caucvgrelemcau  11760  caucvgre  11761  cvg1nlemcau  11764  cvg1nlemres  11765  recvguniq  11775  resqrexlemover  11790  resqrexlemgt0  11800  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemsqa  11804  resqrexlemex  11805  maxleastlt  11996  minmax  12011  lemininf  12015  ltmininf  12016  xrmaxleastlt  12038  xrmaxltsup  12040  xrminmax  12047  xrmin1inf  12049  xrmin2inf  12050  xrltmininf  12052  xrlemininf  12053  climserle  12127  summodclem3  12163  summodclem2a  12164  summodc  12166  zsumdc  12167  fsum3  12170  fsum00  12245  fsumabs  12248  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  zproddc  12362  fprodseq  12366  fprodle  12423  sin01bnd  12540  cos01bnd  12541  summodnegmod  12605  modmulconst  12606  dvdsaddr  12620  dvdssub  12621  dvdssubr  12622  dvdslelemd  12626  dvdsfac  12643  dvdsmod  12645  oddp1even  12659  ltoddhalfle  12676  opoe  12678  omoe  12679  divalg2  12709  divalgmod  12710  ndvdssub  12713  ndvdsadd  12714  bitsfval  12725  bitsval  12726  bits0  12731  bitsp1  12734  bitsfzolem  12737  bitsfzo  12738  bitscmp  12741  bitsinv1lem  12744  bezoutlembi  12798  dvdssqim  12817  dvdsmulgcd  12818  dvdssq  12824  nn0seqcvgd  12835  coprmdvds  12886  coprmdvds2  12887  rpmul  12892  cncongr1  12897  divgcdodd  12938  isprm6  12942  prmdvdsexp  12943  prmdvdsexpr  12945  prmfac1  12947  nnmaxpwlemxy  12964  nnmaxpwlemnfac  12967  sqpweven  12971  2sqpwodd  12972  sqne2sq  12973  hashdvds  13019  phiprmpw  13020  eulerthlemh  13029  prmdiv  13033  prmdiveq  13034  odzval  13040  odzcllem  13041  odzdvds  13044  pythagtriplem11  13073  pythagtriplem13  13075  pythagtrip  13082  pceulem  13093  pczndvds2  13117  pcdvdsb  13119  pc2dvds  13129  pcz  13131  pcprmpw2  13132  dvdsprmpweq  13134  dvdsprmpweqle  13136  difsqpwdvds  13137  pcmpt  13142  prmpwdvds  13154  pockthlem  13155  4sqlem11  13200  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfileme  13285  ballotfilemefi  13286  ballotfilemodife  13289  ballotfilem4  13290  ballotfilem1c  13300  ballotfilemsval  13301  ballotfilemieq  13309  ballotfilemfrcn0  13322  ballotfi  13331  exmidunben  13366  nninfdclemlt  13391  mulgval  13974  dvdsrtr  14457  dvdsrmul1  14458  unitnegcl  14486  unitpropdg  14504  elrhmunit  14533  zndvds0  15034  znunit  15043  mplsubgfilemcl  15139  psmettri2  15478  ismet2  15504  xmettri2  15511  comet  15649  ivthinclemum  15785  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemdisj  15790  ivthinclemloc  15791  ivthinc  15793  ivthreinc  15795  limccl  15809  ellimc3apf  15810  sin0pilem2  15933  pilem3  15934  sincosq1sgn  15977  sincosq2sgn  15978  sincosq4sgn  15980  logltb  16026  logle1b  16044  loglt1b  16045  logbgt0b  16121  wilthlem1  16151  sgmval  16164  dvdsppwf1o  16184  perfect1  16196  bcmono  16202  bclbnd  16205  bposlem1  16209  bposlem5  16213  lgslem1  16217  lgsval  16221  lgsdilem  16244  lgsne0  16255  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  lgseisenlem1  16287  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem2  16299  m1lgs  16302  2lgslem1a1  16303  2lgslem1a  16305  2lgsoddprmlem2  16323  2lgsoddprmlem3  16328  2sqlem4  16335  2sqlem8a  16339  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  eupth2lem3lem7fi  16813  eupth2lemsfi  16817  eupth2fi  16818  konigsberglem4  16830