Theorem breq2d 4095

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breqtrd  4109  sbcbr1g  4140  pofun  4403  csbfv12g  5669  isorel  5938  isocnv  5941  isotr  5946  caovordig  6177  caovordg  6179  caovord  6183  xporderlem  6383  th3qlem2  6793  phplem3g  7025  supsnti  7183  inflbti  7202  difinfinf  7279  enqdc1  7560  ltanqg  7598  ltmnqg  7599  archnqq  7615  prarloclemarch2  7617  prloc  7689  addnqprllem  7725  addlocprlemgt  7732  appdivnq  7761  mulnqprl  7766  1idprl  7788  ltexprlemloc  7805  caucvgprlemcanl  7842  cauappcvgprlemm  7843  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlemlim  7859  cauappcvgpr  7860  archrecnq  7861  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemcl  7874  caucvgprlemladdrl  7876  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgprpr  7910  ltposr  7961  ltasrg  7968  mulgt0sr  7976  mulextsr1lem  7978  mulextsr1  7979  prsrlt  7985  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsrlembound  7992  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  caucvgsr  8000  map2psrprg  8003  pitonnlem2  8045  pitonn  8046  recidpipr  8054  axpre-ltadd  8084  axpre-mulgt0  8085  axpre-mulext  8086  axarch  8089  nntopi  8092  axcaucvglemval  8095  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  ltaddneg  8582  ltsubadd2  8591  lesubadd2  8593  ltaddsub  8594  leaddsub  8596  ltaddpos2  8611  posdif  8613  lesub1  8614  ltsub1  8616  ltnegcon1  8621  lenegcon1  8624  addge02  8631  leaddle0  8635  ltordlem  8640  possumd  8727  sublt0d  8728  apreap  8745  prodgt02  9011  prodge02  9013  ltmulgt12  9023  lemulge12  9025  ltdivmul  9034  ledivmul  9035  ltdivmul2  9036  lt2mul2div  9037  ledivmul2  9038  ltrec  9041  ltrec1  9046  ltdiv23  9050  lediv23  9051  nnge1  9144  halfpos  9353  lt2halves  9358  addltmul  9359  avglt2  9362  avgle2  9364  nnrecl  9378  zltlem1  9515  difgtsumgt  9527  nn0le2is012  9540  gtndiv  9553  qapne  9846  nnledivrp  9974  xltnegi  10043  xltadd1  10084  xsubge0  10089  xposdif  10090  xlesubadd  10091  xleaddadd  10095  divelunit  10210  eluzgtdifelfzo  10415  qtri3or  10472  exbtwnzlemstep  10479  exbtwnzlemshrink  10480  exbtwnzlemex  10481  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2zlemshrink  10485  rebtwn2z  10486  flqlelt  10508  flqbi  10522  2tnp1ge0ge0  10533  q2submod  10619  frec2uzltd  10637  frec2uzlt2d  10638  frec2uzf1od  10640  monoord  10719  ser3mono  10721  ser3ge0  10770  expnbnd  10897  nn0ltexp2  10943  facwordi  10974  hashunlem  11038  zfz1isolemiso  11074  seq3coll  11077  swrdccat3blem  11286  caucvgrelemcau  11506  caucvgre  11507  cvg1nlemcau  11510  cvg1nlemres  11511  recvguniq  11521  resqrexlemover  11536  resqrexlemgt0  11546  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemsqa  11550  resqrexlemex  11551  maxleastlt  11741  minmax  11756  lemininf  11760  ltmininf  11761  xrmaxleastlt  11782  xrmaxltsup  11784  xrminmax  11791  xrmin1inf  11793  xrmin2inf  11794  xrltmininf  11796  xrlemininf  11797  climserle  11871  summodclem3  11906  summodclem2a  11907  summodc  11909  zsumdc  11910  fsum3  11913  fsum00  11988  fsumabs  11991  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  zproddc  12105  fprodseq  12109  fprodle  12166  sin01bnd  12283  cos01bnd  12284  summodnegmod  12348  modmulconst  12349  dvdsaddr  12363  dvdssub  12364  dvdssubr  12365  dvdslelemd  12369  dvdsfac  12386  dvdsmod  12388  oddp1even  12402  ltoddhalfle  12419  opoe  12421  omoe  12422  divalg2  12452  divalgmod  12453  ndvdssub  12456  ndvdsadd  12457  bitsfval  12468  bitsval  12469  bits0  12474  bitsp1  12477  bitsfzolem  12480  bitsfzo  12481  bitscmp  12484  bitsinv1lem  12487  bezoutlembi  12541  dvdssqim  12560  dvdsmulgcd  12561  dvdssq  12567  nn0seqcvgd  12578  coprmdvds  12629  coprmdvds2  12630  rpmul  12635  cncongr1  12640  divgcdodd  12680  isprm6  12684  prmdvdsexp  12685  prmdvdsexpr  12687  prmfac1  12689  oddpwdclemxy  12706  oddpwdclemodd  12709  sqpweven  12712  2sqpwodd  12713  sqne2sq  12714  hashdvds  12758  phiprmpw  12759  eulerthlemh  12768  prmdiv  12772  prmdiveq  12773  odzval  12779  odzcllem  12780  odzdvds  12783  pythagtriplem11  12812  pythagtriplem13  12814  pythagtrip  12821  pceulem  12832  pczndvds2  12856  pcdvdsb  12858  pc2dvds  12868  pcz  12870  pcprmpw2  12871  dvdsprmpweq  12873  dvdsprmpweqle  12875  difsqpwdvds  12876  pcmpt  12881  prmpwdvds  12893  pockthlem  12894  4sqlem11  12939  exmidunben  13012  nninfdclemlt  13037  mulgval  13674  dvdsrtr  14080  dvdsrmul1  14081  unitnegcl  14109  unitpropdg  14127  elrhmunit  14156  zndvds0  14629  znunit  14638  mplsubgfilemcl  14678  psmettri2  15017  ismet2  15043  xmettri2  15050  comet  15188  ivthinclemum  15324  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemdisj  15329  ivthinclemloc  15330  ivthinc  15332  ivthreinc  15334  limccl  15348  ellimc3apf  15349  sin0pilem2  15471  pilem3  15472  sincosq1sgn  15515  sincosq2sgn  15516  sincosq4sgn  15518  logltb  15563  logle1b  15581  loglt1b  15582  logbgt0b  15655  wilthlem1  15669  sgmval  15672  dvdsppwf1o  15678  perfect1  15687  lgslem1  15694  lgsval  15698  lgsdilem  15721  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  lgseisenlem1  15764  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem2  15776  m1lgs  15779  2lgslem1a1  15780  2lgslem1a  15782  2lgsoddprmlem2  15800  2lgsoddprmlem3  15805  2sqlem4  15812  2sqlem8a  15816