Theorem breq2d 4071

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   class class class wbr 4059

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  breqtrd  4085  sbcbr1g  4116  pofun  4377  csbfv12g  5637  isorel  5900  isocnv  5903  isotr  5908  caovordig  6135  caovordg  6137  caovord  6141  xporderlem  6340  th3qlem2  6748  phplem3g  6978  supsnti  7133  inflbti  7152  difinfinf  7229  enqdc1  7510  ltanqg  7548  ltmnqg  7549  archnqq  7565  prarloclemarch2  7567  prloc  7639  addnqprllem  7675  addlocprlemgt  7682  appdivnq  7711  mulnqprl  7716  1idprl  7738  ltexprlemloc  7755  caucvgprlemcanl  7792  cauappcvgprlemm  7793  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlemlim  7809  cauappcvgpr  7810  archrecnq  7811  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemcl  7824  caucvgprlemladdrl  7826  caucvgpr  7830  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnkeqj  7838  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  caucvgprprlem1  7857  caucvgprprlem2  7858  caucvgprpr  7860  ltposr  7911  ltasrg  7918  mulgt0sr  7926  mulextsr1lem  7928  mulextsr1  7929  prsrlt  7935  caucvgsrlemcl  7937  caucvgsrlemfv  7939  caucvgsrlembound  7942  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  caucvgsr  7950  map2psrprg  7953  pitonnlem2  7995  pitonn  7996  recidpipr  8004  axpre-ltadd  8034  axpre-mulgt0  8035  axpre-mulext  8036  axarch  8039  nntopi  8042  axcaucvglemval  8045  axcaucvglemcau  8046  axcaucvglemres  8047  axpre-suploclemres  8049  ltaddneg  8532  ltsubadd2  8541  lesubadd2  8543  ltaddsub  8544  leaddsub  8546  ltaddpos2  8561  posdif  8563  lesub1  8564  ltsub1  8566  ltnegcon1  8571  lenegcon1  8574  addge02  8581  leaddle0  8585  ltordlem  8590  possumd  8677  sublt0d  8678  apreap  8695  prodgt02  8961  prodge02  8963  ltmulgt12  8973  lemulge12  8975  ltdivmul  8984  ledivmul  8985  ltdivmul2  8986  lt2mul2div  8987  ledivmul2  8988  ltrec  8991  ltrec1  8996  ltdiv23  9000  lediv23  9001  nnge1  9094  halfpos  9303  lt2halves  9308  addltmul  9309  avglt2  9312  avgle2  9314  nnrecl  9328  zltlem1  9465  difgtsumgt  9477  nn0le2is012  9490  gtndiv  9503  qapne  9795  nnledivrp  9923  xltnegi  9992  xltadd1  10033  xsubge0  10038  xposdif  10039  xlesubadd  10040  xleaddadd  10044  divelunit  10159  eluzgtdifelfzo  10363  qtri3or  10420  exbtwnzlemstep  10427  exbtwnzlemshrink  10428  exbtwnzlemex  10429  exbtwnz  10430  rebtwn2zlemstep  10432  rebtwn2zlemshrink  10433  rebtwn2z  10434  flqlelt  10456  flqbi  10470  2tnp1ge0ge0  10481  q2submod  10567  frec2uzltd  10585  frec2uzlt2d  10586  frec2uzf1od  10588  monoord  10667  ser3mono  10669  ser3ge0  10718  expnbnd  10845  nn0ltexp2  10891  facwordi  10922  hashunlem  10986  zfz1isolemiso  11021  seq3coll  11024  swrdccat3blem  11230  caucvgrelemcau  11406  caucvgre  11407  cvg1nlemcau  11410  cvg1nlemres  11411  recvguniq  11421  resqrexlemover  11436  resqrexlemgt0  11446  resqrexlemoverl  11447  resqrexlemglsq  11448  resqrexlemsqa  11450  resqrexlemex  11451  maxleastlt  11641  minmax  11656  lemininf  11660  ltmininf  11661  xrmaxleastlt  11682  xrmaxltsup  11684  xrminmax  11691  xrmin1inf  11693  xrmin2inf  11694  xrltmininf  11696  xrlemininf  11697  climserle  11771  summodclem3  11806  summodclem2a  11807  summodc  11809  zsumdc  11810  fsum3  11813  fsum00  11888  fsumabs  11891  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  zproddc  12005  fprodseq  12009  fprodle  12066  sin01bnd  12183  cos01bnd  12184  summodnegmod  12248  modmulconst  12249  dvdsaddr  12263  dvdssub  12264  dvdssubr  12265  dvdslelemd  12269  dvdsfac  12286  dvdsmod  12288  oddp1even  12302  ltoddhalfle  12319  opoe  12321  omoe  12322  divalg2  12352  divalgmod  12353  ndvdssub  12356  ndvdsadd  12357  bitsfval  12368  bitsval  12369  bits0  12374  bitsp1  12377  bitsfzolem  12380  bitsfzo  12381  bitscmp  12384  bitsinv1lem  12387  bezoutlembi  12441  dvdssqim  12460  dvdsmulgcd  12461  dvdssq  12467  nn0seqcvgd  12478  coprmdvds  12529  coprmdvds2  12530  rpmul  12535  cncongr1  12540  divgcdodd  12580  isprm6  12584  prmdvdsexp  12585  prmdvdsexpr  12587  prmfac1  12589  oddpwdclemxy  12606  oddpwdclemodd  12609  sqpweven  12612  2sqpwodd  12613  sqne2sq  12614  hashdvds  12658  phiprmpw  12659  eulerthlemh  12668  prmdiv  12672  prmdiveq  12673  odzval  12679  odzcllem  12680  odzdvds  12683  pythagtriplem11  12712  pythagtriplem13  12714  pythagtrip  12721  pceulem  12732  pczndvds2  12756  pcdvdsb  12758  pc2dvds  12768  pcz  12770  pcprmpw2  12771  dvdsprmpweq  12773  dvdsprmpweqle  12775  difsqpwdvds  12776  pcmpt  12781  prmpwdvds  12793  pockthlem  12794  4sqlem11  12839  exmidunben  12912  nninfdclemlt  12937  mulgval  13573  dvdsrtr  13978  dvdsrmul1  13979  unitnegcl  14007  unitpropdg  14025  elrhmunit  14054  zndvds0  14527  znunit  14536  mplsubgfilemcl  14576  psmettri2  14915  ismet2  14941  xmettri2  14948  comet  15086  ivthinclemum  15222  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemdisj  15227  ivthinclemloc  15228  ivthinc  15230  ivthreinc  15232  limccl  15246  ellimc3apf  15247  sin0pilem2  15369  pilem3  15370  sincosq1sgn  15413  sincosq2sgn  15414  sincosq4sgn  15416  logltb  15461  logle1b  15479  loglt1b  15480  logbgt0b  15553  wilthlem1  15567  sgmval  15570  dvdsppwf1o  15576  perfect1  15585  lgslem1  15592  lgsval  15596  lgsdilem  15619  lgsne0  15630  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  lgseisenlem1  15662  lgseisenlem2  15663  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem2  15674  m1lgs  15677  2lgslem1a1  15678  2lgslem1a  15680  2lgsoddprmlem2  15698  2lgsoddprmlem3  15703  2sqlem4  15710  2sqlem8a  15714