Theorem breq2d 4126

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   class class class wbr 4114

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  breqtrd  4140  sbcbr1g  4171  pofun  4438  csbfv12g  5715  isorel  5987  isocnv  5990  isotr  5995  caovordig  6228  caovordg  6230  caovord  6234  xporderlem  6440  th3qlem2  6885  phplem3g  7123  supsnti  7309  inflbti  7328  difinfinf  7405  enqdc1  7693  ltanqg  7731  ltmnqg  7732  archnqq  7748  prarloclemarch2  7750  prloc  7822  addnqprllem  7858  addlocprlemgt  7865  appdivnq  7894  mulnqprl  7899  1idprl  7921  ltexprlemloc  7938  caucvgprlemcanl  7975  cauappcvgprlemm  7976  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  cauappcvgpr  7993  archrecnq  7994  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemcl  8007  caucvgprlemladdrl  8009  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem1  8040  caucvgprprlem2  8041  caucvgprpr  8043  ltposr  8094  ltasrg  8101  mulgt0sr  8109  mulextsr1lem  8111  mulextsr1  8112  prsrlt  8118  caucvgsrlemcl  8120  caucvgsrlemfv  8122  caucvgsrlembound  8125  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  map2psrprg  8136  pitonnlem2  8178  pitonn  8179  recidpipr  8187  axpre-ltadd  8217  axpre-mulgt0  8218  axpre-mulext  8219  axarch  8222  nntopi  8225  axcaucvglemval  8228  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  ltaddneg  8715  ltsubadd2  8724  lesubadd2  8726  ltaddsub  8727  leaddsub  8729  ltaddpos2  8744  posdif  8746  lesub1  8747  ltsub1  8749  ltnegcon1  8754  lenegcon1  8757  addge02  8764  leaddle0  8768  ltordlem  8773  possumd  8860  sublt0d  8861  apreap  8878  prodgt02  9144  prodge02  9146  ltmulgt12  9156  lemulge12  9158  ltdivmul  9167  ledivmul  9168  ltdivmul2  9169  lt2mul2div  9170  ledivmul2  9171  ltrec  9174  ltrec1  9179  ltdiv23  9183  lediv23  9184  nnge1  9277  halfpos  9486  lt2halves  9491  addltmul  9492  avglt2  9495  avgle2  9497  nnrecl  9511  zltlem1  9652  difgtsumgt  9664  nn0le2is012  9678  gtndiv  9691  qapne  9989  nnledivrp  10117  xltnegi  10187  xltadd1  10228  xsubge0  10233  xposdif  10234  xlesubadd  10235  xleaddadd  10239  divelunit  10354  eluzgtdifelfzo  10564  qtri3or  10624  exbtwnzlemstep  10631  exbtwnzlemshrink  10632  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2zlemshrink  10637  rebtwn2z  10638  flqlelt  10660  flqbi  10674  2tnp1ge0ge0  10685  q2submod  10771  frec2uzltd  10789  frec2uzlt2d  10790  frec2uzf1od  10792  monoord  10871  ser3mono  10873  ser3ge0  10922  expnbnd  11050  nn0ltexp2  11096  facwordi  11127  hashunlem  11193  ssenneg  11229  zfz1isolemiso  11236  seq3coll  11239  swrdccat3blem  11456  caucvgrelemcau  11690  caucvgre  11691  cvg1nlemcau  11694  cvg1nlemres  11695  recvguniq  11705  resqrexlemover  11720  resqrexlemgt0  11730  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemsqa  11734  resqrexlemex  11735  maxleastlt  11925  minmax  11940  lemininf  11944  ltmininf  11945  xrmaxleastlt  11966  xrmaxltsup  11968  xrminmax  11975  xrmin1inf  11977  xrmin2inf  11978  xrltmininf  11980  xrlemininf  11981  climserle  12055  summodclem3  12091  summodclem2a  12092  summodc  12094  zsumdc  12095  fsum3  12098  fsum00  12173  fsumabs  12176  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  zproddc  12290  fprodseq  12294  fprodle  12351  sin01bnd  12468  cos01bnd  12469  summodnegmod  12533  modmulconst  12534  dvdsaddr  12548  dvdssub  12549  dvdssubr  12550  dvdslelemd  12554  dvdsfac  12571  dvdsmod  12573  oddp1even  12587  ltoddhalfle  12604  opoe  12606  omoe  12607  divalg2  12637  divalgmod  12638  ndvdssub  12641  ndvdsadd  12642  bitsfval  12653  bitsval  12654  bits0  12659  bitsp1  12662  bitsfzolem  12665  bitsfzo  12666  bitscmp  12669  bitsinv1lem  12672  bezoutlembi  12726  dvdssqim  12745  dvdsmulgcd  12746  dvdssq  12752  nn0seqcvgd  12763  coprmdvds  12814  coprmdvds2  12815  rpmul  12820  cncongr1  12825  divgcdodd  12865  isprm6  12869  prmdvdsexp  12870  prmdvdsexpr  12872  prmfac1  12874  oddpwdclemxy  12891  oddpwdclemodd  12894  sqpweven  12897  2sqpwodd  12898  sqne2sq  12899  hashdvds  12943  phiprmpw  12944  eulerthlemh  12953  prmdiv  12957  prmdiveq  12958  odzval  12964  odzcllem  12965  odzdvds  12968  pythagtriplem11  12997  pythagtriplem13  12999  pythagtrip  13006  pceulem  13017  pczndvds2  13041  pcdvdsb  13043  pc2dvds  13053  pcz  13055  pcprmpw2  13056  dvdsprmpweq  13058  dvdsprmpweqle  13060  difsqpwdvds  13061  pcmpt  13066  prmpwdvds  13078  pockthlem  13079  4sqlem11  13124  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfileme  13180  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilem4  13185  ballotfilem1c  13195  ballotfilemsval  13196  ballotfilemieq  13204  ballotfilemfrcn0  13217  ballotfi  13226  exmidunben  13261  nninfdclemlt  13286  mulgval  13875  dvdsrtr  14346  dvdsrmul1  14347  unitnegcl  14375  unitpropdg  14393  elrhmunit  14422  zndvds0  14924  znunit  14933  mplsubgfilemcl  14980  psmettri2  15319  ismet2  15345  xmettri2  15352  comet  15490  ivthinclemum  15626  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemdisj  15631  ivthinclemloc  15632  ivthinc  15634  ivthreinc  15636  limccl  15650  ellimc3apf  15651  sin0pilem2  15773  pilem3  15774  sincosq1sgn  15817  sincosq2sgn  15818  sincosq4sgn  15820  logltb  15865  logle1b  15883  loglt1b  15884  logbgt0b  15957  wilthlem1  15974  sgmval  15977  dvdsppwf1o  15983  perfect1  15992  lgslem1  15999  lgsval  16003  lgsdilem  16026  lgsne0  16037  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  lgseisenlem1  16069  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem2  16081  m1lgs  16084  2lgslem1a1  16085  2lgslem1a  16087  2lgsoddprmlem2  16105  2lgsoddprmlem3  16110  2sqlem4  16117  2sqlem8a  16121  eupth2lem3lem3fi  16591  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  eupth2lem3lem7fi  16595  eupth2lemsfi  16599  eupth2fi  16600  konigsberglem4  16612