Theorem breq2d 4016

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   class class class wbr 4004

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  breqtrd  4030  sbcbr1g  4060  pofun  4313  csbfv12g  5552  isorel  5809  isocnv  5812  isotr  5817  caovordig  6040  caovordg  6042  caovord  6046  xporderlem  6232  th3qlem2  6638  phplem3g  6856  supsnti  7004  inflbti  7023  difinfinf  7100  enqdc1  7361  ltanqg  7399  ltmnqg  7400  archnqq  7416  prarloclemarch2  7418  prloc  7490  addnqprllem  7526  addlocprlemgt  7533  appdivnq  7562  mulnqprl  7567  1idprl  7589  ltexprlemloc  7606  caucvgprlemcanl  7643  cauappcvgprlemm  7644  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlemlim  7660  cauappcvgpr  7661  archrecnq  7662  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemcl  7675  caucvgprlemladdrl  7677  caucvgpr  7681  caucvgprprlemell  7684  caucvgprprlemelu  7685  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemnkeqj  7689  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemloc  7702  caucvgprprlemclphr  7704  caucvgprprlemexbt  7705  caucvgprprlem1  7708  caucvgprprlem2  7709  caucvgprpr  7711  ltposr  7762  ltasrg  7769  mulgt0sr  7777  mulextsr1lem  7779  mulextsr1  7780  prsrlt  7786  caucvgsrlemcl  7788  caucvgsrlemfv  7790  caucvgsrlembound  7793  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  caucvgsr  7801  map2psrprg  7804  pitonnlem2  7846  pitonn  7847  recidpipr  7855  axpre-ltadd  7885  axpre-mulgt0  7886  axpre-mulext  7887  axarch  7890  nntopi  7893  axcaucvglemval  7896  axcaucvglemcau  7897  axcaucvglemres  7898  axpre-suploclemres  7900  ltaddneg  8381  ltsubadd2  8390  lesubadd2  8392  ltaddsub  8393  leaddsub  8395  ltaddpos2  8410  posdif  8412  lesub1  8413  ltsub1  8415  ltnegcon1  8420  lenegcon1  8423  addge02  8430  leaddle0  8434  ltordlem  8439  possumd  8526  sublt0d  8527  apreap  8544  prodgt02  8810  prodge02  8812  ltmulgt12  8822  lemulge12  8824  ltdivmul  8833  ledivmul  8834  ltdivmul2  8835  lt2mul2div  8836  ledivmul2  8837  ltrec  8840  ltrec1  8845  ltdiv23  8849  lediv23  8850  nnge1  8942  halfpos  9150  lt2halves  9154  addltmul  9155  avglt2  9158  avgle2  9160  nnrecl  9174  zltlem1  9310  difgtsumgt  9322  nn0le2is012  9335  gtndiv  9348  qapne  9639  nnledivrp  9766  xltnegi  9835  xltadd1  9876  xsubge0  9881  xposdif  9882  xlesubadd  9883  xleaddadd  9887  divelunit  10002  eluzgtdifelfzo  10197  qtri3or  10243  exbtwnzlemstep  10248  exbtwnzlemshrink  10249  exbtwnzlemex  10250  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2zlemshrink  10254  rebtwn2z  10255  flqlelt  10276  flqbi  10290  2tnp1ge0ge0  10301  q2submod  10385  frec2uzltd  10403  frec2uzlt2d  10404  frec2uzf1od  10406  monoord  10476  ser3mono  10478  ser3ge0  10517  expnbnd  10644  nn0ltexp2  10689  facwordi  10720  hashunlem  10784  zfz1isolemiso  10819  seq3coll  10822  caucvgrelemcau  10989  caucvgre  10990  cvg1nlemcau  10993  cvg1nlemres  10994  recvguniq  11004  resqrexlemover  11019  resqrexlemgt0  11029  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemsqa  11033  resqrexlemex  11034  maxleastlt  11224  minmax  11238  lemininf  11242  ltmininf  11243  xrmaxleastlt  11264  xrmaxltsup  11266  xrminmax  11273  xrmin1inf  11275  xrmin2inf  11276  xrltmininf  11278  xrlemininf  11279  climserle  11353  summodclem3  11388  summodclem2a  11389  summodc  11391  zsumdc  11392  fsum3  11395  fsum00  11470  fsumabs  11473  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  zproddc  11587  fprodseq  11591  fprodle  11648  sin01bnd  11765  cos01bnd  11766  summodnegmod  11829  modmulconst  11830  dvdsaddr  11844  dvdssub  11845  dvdssubr  11846  dvdslelemd  11849  dvdsfac  11866  dvdsmod  11868  oddp1even  11881  ltoddhalfle  11898  opoe  11900  omoe  11901  divalg2  11931  divalgmod  11932  ndvdssub  11935  ndvdsadd  11936  bezoutlembi  12006  dvdssqim  12025  dvdsmulgcd  12026  dvdssq  12032  nn0seqcvgd  12041  coprmdvds  12092  coprmdvds2  12093  rpmul  12098  cncongr1  12103  divgcdodd  12143  isprm6  12147  prmdvdsexp  12148  prmdvdsexpr  12150  prmfac1  12152  oddpwdclemxy  12169  oddpwdclemodd  12172  sqpweven  12175  2sqpwodd  12176  sqne2sq  12177  hashdvds  12221  phiprmpw  12222  eulerthlemh  12231  prmdiv  12235  prmdiveq  12236  odzval  12241  odzcllem  12242  odzdvds  12245  pythagtriplem11  12274  pythagtriplem13  12276  pythagtrip  12283  pceulem  12294  pczndvds2  12317  pcdvdsb  12319  pc2dvds  12329  pcz  12331  pcprmpw2  12332  dvdsprmpweq  12334  dvdsprmpweqle  12336  difsqpwdvds  12337  pcmpt  12341  prmpwdvds  12353  pockthlem  12354  exmidunben  12427  nninfdclemlt  12452  mulgval  12986  dvdsrtr  13270  dvdsrmul1  13271  unitnegcl  13299  unitpropdg  13317  psmettri2  13831  ismet2  13857  xmettri2  13864  comet  14002  ivthinclemum  14116  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemdisj  14121  ivthinclemloc  14122  ivthinc  14124  limccl  14131  ellimc3apf  14132  sin0pilem2  14206  pilem3  14207  sincosq1sgn  14250  sincosq2sgn  14251  sincosq4sgn  14253  logltb  14298  logle1b  14316  loglt1b  14317  logbgt0b  14387  lgslem1  14404  lgsval  14408  lgsdilem  14431  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2lgsoddprmlem2  14457  2lgsoddprmlem3  14462  2sqlem4  14468  2sqlem8a  14472