Theorem breq2d 3834

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

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1287   class class class wbr 3822

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-br 3823

This theorem is referenced by:  breqtrd  3846  sbcbr1g  3873  pofun  4115  csbfv12g  5305  isorel  5550  isocnv  5553  isotr  5558  caovordig  5769  caovordg  5771  caovord  5775  xporderlem  5955  th3qlem2  6349  phplem3g  6526  supsnti  6647  inflbti  6666  enqdc1  6868  ltanqg  6906  ltmnqg  6907  archnqq  6923  prarloclemarch2  6925  prloc  6997  addnqprllem  7033  addlocprlemgt  7040  appdivnq  7069  mulnqprl  7074  1idprl  7096  ltexprlemloc  7113  caucvgprlemcanl  7150  cauappcvgprlemm  7151  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem1  7165  cauappcvgprlemlim  7167  cauappcvgpr  7168  archrecnq  7169  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemm  7174  caucvgprlemcl  7182  caucvgprlemladdrl  7184  caucvgpr  7188  caucvgprprlemell  7191  caucvgprprlemelu  7192  caucvgprprlemcbv  7193  caucvgprprlemval  7194  caucvgprprlemnkeqj  7196  caucvgprprlemml  7200  caucvgprprlemmu  7201  caucvgprprlemopl  7203  caucvgprprlemlol  7204  caucvgprprlemopu  7205  caucvgprprlemloc  7209  caucvgprprlemclphr  7211  caucvgprprlemexbt  7212  caucvgprprlem1  7215  caucvgprprlem2  7216  caucvgprpr  7218  ltposr  7256  ltasrg  7263  mulgt0sr  7270  mulextsr1lem  7272  mulextsr1  7273  prsrlt  7279  caucvgsrlemcl  7281  caucvgsrlemfv  7283  caucvgsrlembound  7286  caucvgsrlemgt1  7287  caucvgsrlemoffres  7292  caucvgsr  7294  pitonnlem2  7331  pitonn  7332  recidpipr  7340  axpre-ltadd  7368  axpre-mulgt0  7369  axpre-mulext  7370  axarch  7373  nntopi  7376  axcaucvglemval  7379  axcaucvglemcau  7380  axcaucvglemres  7381  ltaddneg  7849  ltsubadd2  7858  lesubadd2  7860  ltaddsub  7861  leaddsub  7863  ltaddpos2  7878  posdif  7880  lesub1  7881  ltsub1  7883  ltnegcon1  7888  lenegcon1  7891  addge02  7898  leaddle0  7902  possumd  7990  sublt0d  7991  apreap  8008  prodgt02  8252  prodge02  8254  ltmulgt12  8264  lemulge12  8266  ltdivmul  8275  ledivmul  8276  ltdivmul2  8277  lt2mul2div  8278  ledivmul2  8279  ltrec  8282  ltrec1  8287  ltdiv23  8291  lediv23  8292  nnge1  8383  halfpos  8583  lt2halves  8587  addltmul  8588  avglt2  8591  avgle2  8593  nnrecl  8607  zltlem1  8743  gtndiv  8777  qapne  9059  nnledivrp  9172  xltnegi  9232  divelunit  9354  eluzgtdifelfzo  9539  qtri3or  9585  exbtwnzlemstep  9590  exbtwnzlemshrink  9591  exbtwnzlemex  9592  exbtwnz  9593  rebtwn2zlemstep  9595  rebtwn2zlemshrink  9596  rebtwn2z  9597  flqlelt  9614  flqbi  9628  2tnp1ge0ge0  9639  q2submod  9723  frec2uzltd  9741  frec2uzlt2d  9742  frec2uzf1od  9744  monoord  9829  isermono  9831  ser3ge0  9872  expnbnd  9995  facwordi  10066  hashunlem  10130  zfz1isolemiso  10162  iseqcoll  10165  caucvgrelemcau  10330  caucvgre  10331  cvg1nlemcau  10334  cvg1nlemres  10335  recvguniq  10345  resqrexlemover  10360  resqrexlemgt0  10370  resqrexlemoverl  10371  resqrexlemglsq  10372  resqrexlemsqa  10374  resqrexlemex  10375  maxleastlt  10565  minmax  10577  lemininf  10580  ltmininf  10581  climserile  10649  isummolem3  10683  isummolem2a  10684  isummo  10686  zisum  10687  fisum  10689  summodnegmod  10752  modmulconst  10753  dvdsaddr  10765  dvdssub  10766  dvdssubr  10767  dvdslelemd  10769  dvdsfac  10786  dvdsmod  10788  oddp1even  10801  ltoddhalfle  10818  opoe  10820  omoe  10821  divalg2  10851  divalgmod  10852  ndvdssub  10855  ndvdsadd  10856  bezoutlembi  10919  dvdssqim  10938  dvdsmulgcd  10939  dvdssq  10945  nn0seqcvgd  10948  coprmdvds  10999  coprmdvds2  11000  rpmul  11005  cncongr1  11010  divgcdodd  11047  isprm6  11051  prmdvdsexp  11052  prmdvdsexpr  11054  prmfac1  11056  oddpwdclemxy  11072  oddpwdclemodd  11075  sqpweven  11078  2sqpwodd  11079  sqne2sq  11080  hashdvds  11122  phiprmpw  11123