Theorem breq2d 4098

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

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

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  breqtrd  4112  sbcbr1g  4143  pofun  4407  csbfv12g  5675  isorel  5944  isocnv  5947  isotr  5952  caovordig  6183  caovordg  6185  caovord  6189  xporderlem  6391  th3qlem2  6802  phplem3g  7037  supsnti  7195  inflbti  7214  difinfinf  7291  enqdc1  7572  ltanqg  7610  ltmnqg  7611  archnqq  7627  prarloclemarch2  7629  prloc  7701  addnqprllem  7737  addlocprlemgt  7744  appdivnq  7773  mulnqprl  7778  1idprl  7800  ltexprlemloc  7817  caucvgprlemcanl  7854  cauappcvgprlemm  7855  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlemlim  7871  cauappcvgpr  7872  archrecnq  7873  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemcl  7886  caucvgprlemladdrl  7888  caucvgpr  7892  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnkeqj  7900  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlemclphr  7915  caucvgprprlemexbt  7916  caucvgprprlem1  7919  caucvgprprlem2  7920  caucvgprpr  7922  ltposr  7973  ltasrg  7980  mulgt0sr  7988  mulextsr1lem  7990  mulextsr1  7991  prsrlt  7997  caucvgsrlemcl  7999  caucvgsrlemfv  8001  caucvgsrlembound  8004  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  caucvgsr  8012  map2psrprg  8015  pitonnlem2  8057  pitonn  8058  recidpipr  8066  axpre-ltadd  8096  axpre-mulgt0  8097  axpre-mulext  8098  axarch  8101  nntopi  8104  axcaucvglemval  8107  axcaucvglemcau  8108  axcaucvglemres  8109  axpre-suploclemres  8111  ltaddneg  8594  ltsubadd2  8603  lesubadd2  8605  ltaddsub  8606  leaddsub  8608  ltaddpos2  8623  posdif  8625  lesub1  8626  ltsub1  8628  ltnegcon1  8633  lenegcon1  8636  addge02  8643  leaddle0  8647  ltordlem  8652  possumd  8739  sublt0d  8740  apreap  8757  prodgt02  9023  prodge02  9025  ltmulgt12  9035  lemulge12  9037  ltdivmul  9046  ledivmul  9047  ltdivmul2  9048  lt2mul2div  9049  ledivmul2  9050  ltrec  9053  ltrec1  9058  ltdiv23  9062  lediv23  9063  nnge1  9156  halfpos  9365  lt2halves  9370  addltmul  9371  avglt2  9374  avgle2  9376  nnrecl  9390  zltlem1  9527  difgtsumgt  9539  nn0le2is012  9552  gtndiv  9565  qapne  9863  nnledivrp  9991  xltnegi  10060  xltadd1  10101  xsubge0  10106  xposdif  10107  xlesubadd  10108  xleaddadd  10112  divelunit  10227  eluzgtdifelfzo  10432  qtri3or  10490  exbtwnzlemstep  10497  exbtwnzlemshrink  10498  exbtwnzlemex  10499  exbtwnz  10500  rebtwn2zlemstep  10502  rebtwn2zlemshrink  10503  rebtwn2z  10504  flqlelt  10526  flqbi  10540  2tnp1ge0ge0  10551  q2submod  10637  frec2uzltd  10655  frec2uzlt2d  10656  frec2uzf1od  10658  monoord  10737  ser3mono  10739  ser3ge0  10788  expnbnd  10915  nn0ltexp2  10961  facwordi  10992  hashunlem  11057  zfz1isolemiso  11093  seq3coll  11096  swrdccat3blem  11310  caucvgrelemcau  11531  caucvgre  11532  cvg1nlemcau  11535  cvg1nlemres  11536  recvguniq  11546  resqrexlemover  11561  resqrexlemgt0  11571  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemsqa  11575  resqrexlemex  11576  maxleastlt  11766  minmax  11781  lemininf  11785  ltmininf  11786  xrmaxleastlt  11807  xrmaxltsup  11809  xrminmax  11816  xrmin1inf  11818  xrmin2inf  11819  xrltmininf  11821  xrlemininf  11822  climserle  11896  summodclem3  11931  summodclem2a  11932  summodc  11934  zsumdc  11935  fsum3  11938  fsum00  12013  fsumabs  12016  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  zproddc  12130  fprodseq  12134  fprodle  12191  sin01bnd  12308  cos01bnd  12309  summodnegmod  12373  modmulconst  12374  dvdsaddr  12388  dvdssub  12389  dvdssubr  12390  dvdslelemd  12394  dvdsfac  12411  dvdsmod  12413  oddp1even  12427  ltoddhalfle  12444  opoe  12446  omoe  12447  divalg2  12477  divalgmod  12478  ndvdssub  12481  ndvdsadd  12482  bitsfval  12493  bitsval  12494  bits0  12499  bitsp1  12502  bitsfzolem  12505  bitsfzo  12506  bitscmp  12509  bitsinv1lem  12512  bezoutlembi  12566  dvdssqim  12585  dvdsmulgcd  12586  dvdssq  12592  nn0seqcvgd  12603  coprmdvds  12654  coprmdvds2  12655  rpmul  12660  cncongr1  12665  divgcdodd  12705  isprm6  12709  prmdvdsexp  12710  prmdvdsexpr  12712  prmfac1  12714  oddpwdclemxy  12731  oddpwdclemodd  12734  sqpweven  12737  2sqpwodd  12738  sqne2sq  12739  hashdvds  12783  phiprmpw  12784  eulerthlemh  12793  prmdiv  12797  prmdiveq  12798  odzval  12804  odzcllem  12805  odzdvds  12808  pythagtriplem11  12837  pythagtriplem13  12839  pythagtrip  12846  pceulem  12857  pczndvds2  12881  pcdvdsb  12883  pc2dvds  12893  pcz  12895  pcprmpw2  12896  dvdsprmpweq  12898  dvdsprmpweqle  12900  difsqpwdvds  12901  pcmpt  12906  prmpwdvds  12918  pockthlem  12919  4sqlem11  12964  exmidunben  13037  nninfdclemlt  13062  mulgval  13699  dvdsrtr  14105  dvdsrmul1  14106  unitnegcl  14134  unitpropdg  14152  elrhmunit  14181  zndvds0  14654  znunit  14663  mplsubgfilemcl  14703  psmettri2  15042  ismet2  15068  xmettri2  15075  comet  15213  ivthinclemum  15349  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemdisj  15354  ivthinclemloc  15355  ivthinc  15357  ivthreinc  15359  limccl  15373  ellimc3apf  15374  sin0pilem2  15496  pilem3  15497  sincosq1sgn  15540  sincosq2sgn  15541  sincosq4sgn  15543  logltb  15588  logle1b  15606  loglt1b  15607  logbgt0b  15680  wilthlem1  15694  sgmval  15697  dvdsppwf1o  15703  perfect1  15712  lgslem1  15719  lgsval  15723  lgsdilem  15746  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  lgseisenlem1  15789  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem2  15801  m1lgs  15804  2lgslem1a1  15805  2lgslem1a  15807  2lgsoddprmlem2  15825  2lgsoddprmlem3  15830  2sqlem4  15837  2sqlem8a  15841