Theorem breq2d 3994

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1343   class class class wbr 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-br 3983

This theorem is referenced by:  breqtrd  4008  sbcbr1g  4038  pofun  4290  csbfv12g  5522  isorel  5776  isocnv  5779  isotr  5784  caovordig  6007  caovordg  6009  caovord  6013  xporderlem  6199  th3qlem2  6604  phplem3g  6822  supsnti  6970  inflbti  6989  difinfinf  7066  enqdc1  7303  ltanqg  7341  ltmnqg  7342  archnqq  7358  prarloclemarch2  7360  prloc  7432  addnqprllem  7468  addlocprlemgt  7475  appdivnq  7504  mulnqprl  7509  1idprl  7531  ltexprlemloc  7548  caucvgprlemcanl  7585  cauappcvgprlemm  7586  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem1  7600  cauappcvgprlemlim  7602  cauappcvgpr  7603  archrecnq  7604  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemm  7609  caucvgprlemcl  7617  caucvgprlemladdrl  7619  caucvgpr  7623  caucvgprprlemell  7626  caucvgprprlemelu  7627  caucvgprprlemcbv  7628  caucvgprprlemval  7629  caucvgprprlemnkeqj  7631  caucvgprprlemml  7635  caucvgprprlemmu  7636  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemopu  7640  caucvgprprlemloc  7644  caucvgprprlemclphr  7646  caucvgprprlemexbt  7647  caucvgprprlem1  7650  caucvgprprlem2  7651  caucvgprpr  7653  ltposr  7704  ltasrg  7711  mulgt0sr  7719  mulextsr1lem  7721  mulextsr1  7722  prsrlt  7728  caucvgsrlemcl  7730  caucvgsrlemfv  7732  caucvgsrlembound  7735  caucvgsrlemgt1  7736  caucvgsrlemoffres  7741  caucvgsr  7743  map2psrprg  7746  pitonnlem2  7788  pitonn  7789  recidpipr  7797  axpre-ltadd  7827  axpre-mulgt0  7828  axpre-mulext  7829  axarch  7832  nntopi  7835  axcaucvglemval  7838  axcaucvglemcau  7839  axcaucvglemres  7840  axpre-suploclemres  7842  ltaddneg  8322  ltsubadd2  8331  lesubadd2  8333  ltaddsub  8334  leaddsub  8336  ltaddpos2  8351  posdif  8353  lesub1  8354  ltsub1  8356  ltnegcon1  8361  lenegcon1  8364  addge02  8371  leaddle0  8375  ltordlem  8380  possumd  8467  sublt0d  8468  apreap  8485  prodgt02  8748  prodge02  8750  ltmulgt12  8760  lemulge12  8762  ltdivmul  8771  ledivmul  8772  ltdivmul2  8773  lt2mul2div  8774  ledivmul2  8775  ltrec  8778  ltrec1  8783  ltdiv23  8787  lediv23  8788  nnge1  8880  halfpos  9088  lt2halves  9092  addltmul  9093  avglt2  9096  avgle2  9098  nnrecl  9112  zltlem1  9248  difgtsumgt  9260  nn0le2is012  9273  gtndiv  9286  qapne  9577  nnledivrp  9702  xltnegi  9771  xltadd1  9812  xsubge0  9817  xposdif  9818  xlesubadd  9819  xleaddadd  9823  divelunit  9938  eluzgtdifelfzo  10132  qtri3or  10178  exbtwnzlemstep  10183  exbtwnzlemshrink  10184  exbtwnzlemex  10185  exbtwnz  10186  rebtwn2zlemstep  10188  rebtwn2zlemshrink  10189  rebtwn2z  10190  flqlelt  10211  flqbi  10225  2tnp1ge0ge0  10236  q2submod  10320  frec2uzltd  10338  frec2uzlt2d  10339  frec2uzf1od  10341  monoord  10411  ser3mono  10413  ser3ge0  10452  expnbnd  10578  nn0ltexp2  10623  facwordi  10653  hashunlem  10717  zfz1isolemiso  10752  seq3coll  10755  caucvgrelemcau  10922  caucvgre  10923  cvg1nlemcau  10926  cvg1nlemres  10927  recvguniq  10937  resqrexlemover  10952  resqrexlemgt0  10962  resqrexlemoverl  10963  resqrexlemglsq  10964  resqrexlemsqa  10966  resqrexlemex  10967  maxleastlt  11157  minmax  11171  lemininf  11175  ltmininf  11176  xrmaxleastlt  11197  xrmaxltsup  11199  xrminmax  11206  xrmin1inf  11208  xrmin2inf  11209  xrltmininf  11211  xrlemininf  11212  climserle  11286  summodclem3  11321  summodclem2a  11322  summodc  11324  zsumdc  11325  fsum3  11328  fsum00  11403  fsumabs  11406  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  zproddc  11520  fprodseq  11524  fprodle  11581  sin01bnd  11698  cos01bnd  11699  summodnegmod  11762  modmulconst  11763  dvdsaddr  11777  dvdssub  11778  dvdssubr  11779  dvdslelemd  11781  dvdsfac  11798  dvdsmod  11800  oddp1even  11813  ltoddhalfle  11830  opoe  11832  omoe  11833  divalg2  11863  divalgmod  11864  ndvdssub  11867  ndvdsadd  11868  bezoutlembi  11938  dvdssqim  11957  dvdsmulgcd  11958  dvdssq  11964  nn0seqcvgd  11973  coprmdvds  12024  coprmdvds2  12025  rpmul  12030  cncongr1  12035  divgcdodd  12075  isprm6  12079  prmdvdsexp  12080  prmdvdsexpr  12082  prmfac1  12084  oddpwdclemxy  12101  oddpwdclemodd  12104  sqpweven  12107  2sqpwodd  12108  sqne2sq  12109  hashdvds  12153  phiprmpw  12154  eulerthlemh  12163  prmdiv  12167  prmdiveq  12168  odzval  12173  odzcllem  12174  odzdvds  12177  pythagtriplem11  12206  pythagtriplem13  12208  pythagtrip  12215  pceulem  12226  pczndvds2  12249  pcdvdsb  12251  pc2dvds  12261  pcz  12263  pcprmpw2  12264  dvdsprmpweq  12266  dvdsprmpweqle  12268  difsqpwdvds  12269  pcmpt  12273  prmpwdvds  12285  pockthlem  12286  exmidunben  12359  nninfdclemlt  12384  psmettri2  12978  ismet2  13004  xmettri2  13011  comet  13149  ivthinclemum  13263  ivthinclemlopn  13264  ivthinclemlr  13265  ivthinclemuopn  13266  ivthinclemur  13267  ivthinclemdisj  13268  ivthinclemloc  13269  ivthinc  13271  limccl  13278  ellimc3apf  13279  sin0pilem2  13353  pilem3  13354  sincosq1sgn  13397  sincosq2sgn  13398  sincosq4sgn  13400  logltb  13445  logle1b  13463  loglt1b  13464  logbgt0b  13534  lgslem1  13551  lgsval  13555  lgsdilem  13578  lgsne0  13589  2sqlem4  13604  2sqlem8a  13608