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  7346  inflbti  7365  difinfinf  7442  enqdc1  7730  ltanqg  7768  ltmnqg  7769  archnqq  7785  prarloclemarch2  7787  prloc  7859  addnqprllem  7895  addlocprlemgt  7902  appdivnq  7931  mulnqprl  7936  1idprl  7958  ltexprlemloc  7975  caucvgprlemcanl  8012  cauappcvgprlemm  8013  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlemlim  8029  cauappcvgpr  8030  archrecnq  8031  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemcl  8044  caucvgprlemladdrl  8046  caucvgpr  8050  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkeqj  8058  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlem1  8077  caucvgprprlem2  8078  caucvgprpr  8080  ltposr  8131  ltasrg  8138  mulgt0sr  8146  mulextsr1lem  8148  mulextsr1  8149  prsrlt  8155  caucvgsrlemcl  8157  caucvgsrlemfv  8159  caucvgsrlembound  8162  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  caucvgsr  8170  map2psrprg  8173  pitonnlem2  8215  pitonn  8216  recidpipr  8224  axpre-ltadd  8254  axpre-mulgt0  8255  axpre-mulext  8256  axarch  8259  nntopi  8262  axcaucvglemval  8265  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  ltaddneg  8754  ltsubadd2  8763  lesubadd2  8765  ltaddsub  8766  leaddsub  8768  ltaddpos2  8783  posdif  8785  lesub1  8786  ltsub1  8788  ltnegcon1  8793  lenegcon1  8796  addge02  8803  leaddle0  8807  ltordlem  8812  possumd  8900  sublt0d  8901  apreap  8918  prodgt02  9186  prodge02  9188  ltmulgt12  9198  lemulge12  9200  ltdivmul  9209  ledivmul  9210  ltdivmul2  9211  lt2mul2div  9212  ledivmul2  9213  ltrec  9216  ltrec1  9221  ltdiv23  9225  lediv23  9226  nnge1  9330  halfpos  9541  lt2halves  9546  addltmul  9547  avglt2  9550  avgle2  9552  nnrecl  9566  zltlem1  9707  difgtsumgt  9719  nn0le2is012  9733  gtndiv  9746  qapne  10049  nnledivrp  10178  xltnegi  10248  xltadd1  10289  xsubge0  10294  xposdif  10295  xlesubadd  10296  xleaddadd  10300  divelunit  10415  eluzgtdifelfzo  10626  qtri3or  10686  exbtwnzlemstep  10693  exbtwnzlemshrink  10694  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2zlemshrink  10699  rebtwn2z  10700  flqlelt  10723  flaplelt  10724  flqbi  10740  2tnp1ge0ge0  10751  q2submod  10837  frec2uzltd  10855  frec2uzlt2d  10856  frec2uzf1od  10858  monoord  10937  ser3mono  10939  ser3ge0  10988  expnbnd  11116  nn0ltexp2  11163  facwordi  11194  hashunlem  11260  ssenneg  11296  zfz1isolemiso  11307  seq3coll  11310  swrdccat3blem  11527  caucvgrelemcau  11762  caucvgre  11763  cvg1nlemcau  11766  cvg1nlemres  11767  recvguniq  11777  resqrexlemover  11792  resqrexlemgt0  11802  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemsqa  11806  resqrexlemex  11807  maxleastlt  11998  minmax  12014  lemininf  12018  ltmininf  12019  xrmaxleastlt  12041  xrmaxltsup  12043  xrminmax  12050  xrmin1inf  12052  xrmin2inf  12053  xrltmininf  12055  xrlemininf  12056  climserle  12130  summodclem3  12166  summodclem2a  12167  summodc  12169  zsumdc  12170  fsum3  12173  fsum00  12248  fsumabs  12251  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  zproddc  12365  fprodseq  12369  fprodle  12426  sin01bnd  12543  cos01bnd  12544  summodnegmod  12608  modmulconst  12609  dvdsaddr  12623  dvdssub  12624  dvdssubr  12625  dvdslelemd  12629  dvdsfac  12646  dvdsmod  12648  oddp1even  12662  ltoddhalfle  12679  opoe  12681  omoe  12682  divalg2  12712  divalgmod  12713  ndvdssub  12716  ndvdsadd  12717  bitsfval  12728  bitsval  12729  bits0  12734  bitsp1  12737  bitsfzolem  12740  bitsfzo  12741  bitscmp  12744  bitsinv1lem  12747  bezoutlembi  12801  dvdssqim  12820  dvdsmulgcd  12821  dvdssq  12827  nn0seqcvgd  12838  coprmdvds  12889  coprmdvds2  12890  rpmul  12895  cncongr1  12900  divgcdodd  12941  isprm6  12945  prmdvdsexp  12946  prmdvdsexpr  12948  prmfac1  12950  nnmaxpwlemxy  12967  nnmaxpwlemnfac  12970  sqpweven  12974  2sqpwodd  12975  sqne2sq  12976  hashdvds  13022  phiprmpw  13023  eulerthlemh  13032  prmdiv  13036  prmdiveq  13037  odzval  13043  odzcllem  13044  odzdvds  13047  pythagtriplem11  13076  pythagtriplem13  13078  pythagtrip  13085  pceulem  13096  pczndvds2  13120  pcdvdsb  13122  pc2dvds  13132  pcz  13134  pcprmpw2  13135  dvdsprmpweq  13137  dvdsprmpweqle  13139  difsqpwdvds  13140  pcmpt  13145  prmpwdvds  13157  pockthlem  13158  4sqlem11  13203  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfileme  13288  ballotfilemefi  13289  ballotfilemodife  13292  ballotfilem4  13293  ballotfilem1c  13303  ballotfilemsval  13304  ballotfilemieq  13312  ballotfilemfrcn0  13325  ballotfi  13334  exmidunben  13369  nninfdclemlt  13394  mulgval  13978  dvdsrtr  14492  dvdsrmul1  14493  unitnegcl  14521  unitpropdg  14539  elrhmunit  14568  zndvds0  15069  znunit  15078  mplsubgfilemcl  15181  psmettri2  15520  ismet2  15546  xmettri2  15553  comet  15691  ivthinclemum  15827  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemdisj  15832  ivthinclemloc  15833  ivthinc  15835  ivthreinc  15837  limccl  15851  ellimc3apf  15852  sin0pilem2  15975  pilem3  15976  sincosq1sgn  16019  sincosq2sgn  16020  sincosq4sgn  16022  logltb  16068  logle1b  16086  loglt1b  16087  logbgt0b  16163  wilthlem1  16193  sgmval  16213  dvdsppwf1o  16244  chtublem  16256  chtqub  16257  perfect1  16259  bcmono  16265  bclbnd  16268  bposlem1  16272  bposlem5  16276  lgslem1  16285  lgsval  16289  lgsdilem  16312  lgsne0  16323  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  lgseisenlem1  16355  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem2  16367  m1lgs  16370  2lgslem1a1  16371  2lgslem1a  16373  2lgsoddprmlem2  16391  2lgsoddprmlem3  16396  2sqlem4  16403  2sqlem8a  16407  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880  eupth2lem3lem7fi  16881  eupth2lemsfi  16885  eupth2fi  16886  konigsberglem4  16898