Theorem breq2d 4094

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

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

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 4083

This theorem is referenced by:  breqtrd  4108  sbcbr1g  4139  pofun  4402  csbfv12g  5666  isorel  5931  isocnv  5934  isotr  5939  caovordig  6170  caovordg  6172  caovord  6176  xporderlem  6375  th3qlem2  6783  phplem3g  7013  supsnti  7168  inflbti  7187  difinfinf  7264  enqdc1  7545  ltanqg  7583  ltmnqg  7584  archnqq  7600  prarloclemarch2  7602  prloc  7674  addnqprllem  7710  addlocprlemgt  7717  appdivnq  7746  mulnqprl  7751  1idprl  7773  ltexprlemloc  7790  caucvgprlemcanl  7827  cauappcvgprlemm  7828  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlemlim  7844  cauappcvgpr  7845  archrecnq  7846  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemcl  7859  caucvgprlemladdrl  7861  caucvgpr  7865  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemnkeqj  7873  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlemclphr  7888  caucvgprprlemexbt  7889  caucvgprprlem1  7892  caucvgprprlem2  7893  caucvgprpr  7895  ltposr  7946  ltasrg  7953  mulgt0sr  7961  mulextsr1lem  7963  mulextsr1  7964  prsrlt  7970  caucvgsrlemcl  7972  caucvgsrlemfv  7974  caucvgsrlembound  7977  caucvgsrlemgt1  7978  caucvgsrlemoffres  7983  caucvgsr  7985  map2psrprg  7988  pitonnlem2  8030  pitonn  8031  recidpipr  8039  axpre-ltadd  8069  axpre-mulgt0  8070  axpre-mulext  8071  axarch  8074  nntopi  8077  axcaucvglemval  8080  axcaucvglemcau  8081  axcaucvglemres  8082  axpre-suploclemres  8084  ltaddneg  8567  ltsubadd2  8576  lesubadd2  8578  ltaddsub  8579  leaddsub  8581  ltaddpos2  8596  posdif  8598  lesub1  8599  ltsub1  8601  ltnegcon1  8606  lenegcon1  8609  addge02  8616  leaddle0  8620  ltordlem  8625  possumd  8712  sublt0d  8713  apreap  8730  prodgt02  8996  prodge02  8998  ltmulgt12  9008  lemulge12  9010  ltdivmul  9019  ledivmul  9020  ltdivmul2  9021  lt2mul2div  9022  ledivmul2  9023  ltrec  9026  ltrec1  9031  ltdiv23  9035  lediv23  9036  nnge1  9129  halfpos  9338  lt2halves  9343  addltmul  9344  avglt2  9347  avgle2  9349  nnrecl  9363  zltlem1  9500  difgtsumgt  9512  nn0le2is012  9525  gtndiv  9538  qapne  9830  nnledivrp  9958  xltnegi  10027  xltadd1  10068  xsubge0  10073  xposdif  10074  xlesubadd  10075  xleaddadd  10079  divelunit  10194  eluzgtdifelfzo  10398  qtri3or  10455  exbtwnzlemstep  10462  exbtwnzlemshrink  10463  exbtwnzlemex  10464  exbtwnz  10465  rebtwn2zlemstep  10467  rebtwn2zlemshrink  10468  rebtwn2z  10469  flqlelt  10491  flqbi  10505  2tnp1ge0ge0  10516  q2submod  10602  frec2uzltd  10620  frec2uzlt2d  10621  frec2uzf1od  10623  monoord  10702  ser3mono  10704  ser3ge0  10753  expnbnd  10880  nn0ltexp2  10926  facwordi  10957  hashunlem  11021  zfz1isolemiso  11056  seq3coll  11059  swrdccat3blem  11266  caucvgrelemcau  11486  caucvgre  11487  cvg1nlemcau  11490  cvg1nlemres  11491  recvguniq  11501  resqrexlemover  11516  resqrexlemgt0  11526  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemsqa  11530  resqrexlemex  11531  maxleastlt  11721  minmax  11736  lemininf  11740  ltmininf  11741  xrmaxleastlt  11762  xrmaxltsup  11764  xrminmax  11771  xrmin1inf  11773  xrmin2inf  11774  xrltmininf  11776  xrlemininf  11777  climserle  11851  summodclem3  11886  summodclem2a  11887  summodc  11889  zsumdc  11890  fsum3  11893  fsum00  11968  fsumabs  11971  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  zproddc  12085  fprodseq  12089  fprodle  12146  sin01bnd  12263  cos01bnd  12264  summodnegmod  12328  modmulconst  12329  dvdsaddr  12343  dvdssub  12344  dvdssubr  12345  dvdslelemd  12349  dvdsfac  12366  dvdsmod  12368  oddp1even  12382  ltoddhalfle  12399  opoe  12401  omoe  12402  divalg2  12432  divalgmod  12433  ndvdssub  12436  ndvdsadd  12437  bitsfval  12448  bitsval  12449  bits0  12454  bitsp1  12457  bitsfzolem  12460  bitsfzo  12461  bitscmp  12464  bitsinv1lem  12467  bezoutlembi  12521  dvdssqim  12540  dvdsmulgcd  12541  dvdssq  12547  nn0seqcvgd  12558  coprmdvds  12609  coprmdvds2  12610  rpmul  12615  cncongr1  12620  divgcdodd  12660  isprm6  12664  prmdvdsexp  12665  prmdvdsexpr  12667  prmfac1  12669  oddpwdclemxy  12686  oddpwdclemodd  12689  sqpweven  12692  2sqpwodd  12693  sqne2sq  12694  hashdvds  12738  phiprmpw  12739  eulerthlemh  12748  prmdiv  12752  prmdiveq  12753  odzval  12759  odzcllem  12760  odzdvds  12763  pythagtriplem11  12792  pythagtriplem13  12794  pythagtrip  12801  pceulem  12812  pczndvds2  12836  pcdvdsb  12838  pc2dvds  12848  pcz  12850  pcprmpw2  12851  dvdsprmpweq  12853  dvdsprmpweqle  12855  difsqpwdvds  12856  pcmpt  12861  prmpwdvds  12873  pockthlem  12874  4sqlem11  12919  exmidunben  12992  nninfdclemlt  13017  mulgval  13654  dvdsrtr  14059  dvdsrmul1  14060  unitnegcl  14088  unitpropdg  14106  elrhmunit  14135  zndvds0  14608  znunit  14617  mplsubgfilemcl  14657  psmettri2  14996  ismet2  15022  xmettri2  15029  comet  15167  ivthinclemum  15303  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemdisj  15308  ivthinclemloc  15309  ivthinc  15311  ivthreinc  15313  limccl  15327  ellimc3apf  15328  sin0pilem2  15450  pilem3  15451  sincosq1sgn  15494  sincosq2sgn  15495  sincosq4sgn  15497  logltb  15542  logle1b  15560  loglt1b  15561  logbgt0b  15634  wilthlem1  15648  sgmval  15651  dvdsppwf1o  15657  perfect1  15666  lgslem1  15673  lgsval  15677  lgsdilem  15700  lgsne0  15711  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  lgseisenlem1  15743  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem2  15755  m1lgs  15758  2lgslem1a1  15759  2lgslem1a  15761  2lgsoddprmlem2  15779  2lgsoddprmlem3  15784  2sqlem4  15791  2sqlem8a  15795