Theorem breq2d 4042

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   class class class wbr 4030

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031

This theorem is referenced by:  breqtrd  4056  sbcbr1g  4086  pofun  4344  csbfv12g  5593  isorel  5852  isocnv  5855  isotr  5860  caovordig  6086  caovordg  6088  caovord  6092  xporderlem  6286  th3qlem2  6694  phplem3g  6914  supsnti  7066  inflbti  7085  difinfinf  7162  enqdc1  7424  ltanqg  7462  ltmnqg  7463  archnqq  7479  prarloclemarch2  7481  prloc  7553  addnqprllem  7589  addlocprlemgt  7596  appdivnq  7625  mulnqprl  7630  1idprl  7652  ltexprlemloc  7669  caucvgprlemcanl  7706  cauappcvgprlemm  7707  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlemlim  7723  cauappcvgpr  7724  archrecnq  7725  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemcl  7738  caucvgprlemladdrl  7740  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnkeqj  7752  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  caucvgprprlem1  7771  caucvgprprlem2  7772  caucvgprpr  7774  ltposr  7825  ltasrg  7832  mulgt0sr  7840  mulextsr1lem  7842  mulextsr1  7843  prsrlt  7849  caucvgsrlemcl  7851  caucvgsrlemfv  7853  caucvgsrlembound  7856  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  caucvgsr  7864  map2psrprg  7867  pitonnlem2  7909  pitonn  7910  recidpipr  7918  axpre-ltadd  7948  axpre-mulgt0  7949  axpre-mulext  7950  axarch  7953  nntopi  7956  axcaucvglemval  7959  axcaucvglemcau  7960  axcaucvglemres  7961  axpre-suploclemres  7963  ltaddneg  8445  ltsubadd2  8454  lesubadd2  8456  ltaddsub  8457  leaddsub  8459  ltaddpos2  8474  posdif  8476  lesub1  8477  ltsub1  8479  ltnegcon1  8484  lenegcon1  8487  addge02  8494  leaddle0  8498  ltordlem  8503  possumd  8590  sublt0d  8591  apreap  8608  prodgt02  8874  prodge02  8876  ltmulgt12  8886  lemulge12  8888  ltdivmul  8897  ledivmul  8898  ltdivmul2  8899  lt2mul2div  8900  ledivmul2  8901  ltrec  8904  ltrec1  8909  ltdiv23  8913  lediv23  8914  nnge1  9007  halfpos  9216  lt2halves  9221  addltmul  9222  avglt2  9225  avgle2  9227  nnrecl  9241  zltlem1  9377  difgtsumgt  9389  nn0le2is012  9402  gtndiv  9415  qapne  9707  nnledivrp  9835  xltnegi  9904  xltadd1  9945  xsubge0  9950  xposdif  9951  xlesubadd  9952  xleaddadd  9956  divelunit  10071  eluzgtdifelfzo  10267  qtri3or  10313  exbtwnzlemstep  10319  exbtwnzlemshrink  10320  exbtwnzlemex  10321  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2zlemshrink  10325  rebtwn2z  10326  flqlelt  10348  flqbi  10362  2tnp1ge0ge0  10373  q2submod  10459  frec2uzltd  10477  frec2uzlt2d  10478  frec2uzf1od  10480  monoord  10559  ser3mono  10561  ser3ge0  10610  expnbnd  10737  nn0ltexp2  10783  facwordi  10814  hashunlem  10878  zfz1isolemiso  10913  seq3coll  10916  caucvgrelemcau  11127  caucvgre  11128  cvg1nlemcau  11131  cvg1nlemres  11132  recvguniq  11142  resqrexlemover  11157  resqrexlemgt0  11167  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemsqa  11171  resqrexlemex  11172  maxleastlt  11362  minmax  11376  lemininf  11380  ltmininf  11381  xrmaxleastlt  11402  xrmaxltsup  11404  xrminmax  11411  xrmin1inf  11413  xrmin2inf  11414  xrltmininf  11416  xrlemininf  11417  climserle  11491  summodclem3  11526  summodclem2a  11527  summodc  11529  zsumdc  11530  fsum3  11533  fsum00  11608  fsumabs  11611  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  zproddc  11725  fprodseq  11729  fprodle  11786  sin01bnd  11903  cos01bnd  11904  summodnegmod  11968  modmulconst  11969  dvdsaddr  11983  dvdssub  11984  dvdssubr  11985  dvdslelemd  11988  dvdsfac  12005  dvdsmod  12007  oddp1even  12020  ltoddhalfle  12037  opoe  12039  omoe  12040  divalg2  12070  divalgmod  12071  ndvdssub  12074  ndvdsadd  12075  bezoutlembi  12145  dvdssqim  12164  dvdsmulgcd  12165  dvdssq  12171  nn0seqcvgd  12182  coprmdvds  12233  coprmdvds2  12234  rpmul  12239  cncongr1  12244  divgcdodd  12284  isprm6  12288  prmdvdsexp  12289  prmdvdsexpr  12291  prmfac1  12293  oddpwdclemxy  12310  oddpwdclemodd  12313  sqpweven  12316  2sqpwodd  12317  sqne2sq  12318  hashdvds  12362  phiprmpw  12363  eulerthlemh  12372  prmdiv  12376  prmdiveq  12377  odzval  12382  odzcllem  12383  odzdvds  12386  pythagtriplem11  12415  pythagtriplem13  12417  pythagtrip  12424  pceulem  12435  pczndvds2  12459  pcdvdsb  12461  pc2dvds  12471  pcz  12473  pcprmpw2  12474  dvdsprmpweq  12476  dvdsprmpweqle  12478  difsqpwdvds  12479  pcmpt  12484  prmpwdvds  12496  pockthlem  12497  4sqlem11  12542  exmidunben  12586  nninfdclemlt  12611  mulgval  13195  dvdsrtr  13600  dvdsrmul1  13601  unitnegcl  13629  unitpropdg  13647  elrhmunit  13676  zndvds0  14149  znunit  14158  psmettri2  14507  ismet2  14533  xmettri2  14540  comet  14678  ivthinclemum  14814  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemdisj  14819  ivthinclemloc  14820  ivthinc  14822  ivthreinc  14824  limccl  14838  ellimc3apf  14839  sin0pilem2  14958  pilem3  14959  sincosq1sgn  15002  sincosq2sgn  15003  sincosq4sgn  15005  logltb  15050  logle1b  15068  loglt1b  15069  logbgt0b  15139  wilthlem1  15153  lgslem1  15157  lgsval  15161  lgsdilem  15184  lgsne0  15195  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  lgseisenlem1  15227  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem2  15239  m1lgs  15242  2lgslem1a1  15243  2lgslem1a  15245  2lgsoddprmlem2  15263  2lgsoddprmlem3  15268  2sqlem4  15275  2sqlem8a  15279