Theorem breq2d 4046

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   class class class wbr 4034

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  breqtrd  4060  sbcbr1g  4090  pofun  4348  csbfv12g  5599  isorel  5858  isocnv  5861  isotr  5866  caovordig  6093  caovordg  6095  caovord  6099  xporderlem  6298  th3qlem2  6706  phplem3g  6926  supsnti  7080  inflbti  7099  difinfinf  7176  enqdc1  7446  ltanqg  7484  ltmnqg  7485  archnqq  7501  prarloclemarch2  7503  prloc  7575  addnqprllem  7611  addlocprlemgt  7618  appdivnq  7647  mulnqprl  7652  1idprl  7674  ltexprlemloc  7691  caucvgprlemcanl  7728  cauappcvgprlemm  7729  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlemlim  7745  cauappcvgpr  7746  archrecnq  7747  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemcl  7760  caucvgprlemladdrl  7762  caucvgpr  7766  caucvgprprlemell  7769  caucvgprprlemelu  7770  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemnkeqj  7774  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemloc  7787  caucvgprprlemclphr  7789  caucvgprprlemexbt  7790  caucvgprprlem1  7793  caucvgprprlem2  7794  caucvgprpr  7796  ltposr  7847  ltasrg  7854  mulgt0sr  7862  mulextsr1lem  7864  mulextsr1  7865  prsrlt  7871  caucvgsrlemcl  7873  caucvgsrlemfv  7875  caucvgsrlembound  7878  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  caucvgsr  7886  map2psrprg  7889  pitonnlem2  7931  pitonn  7932  recidpipr  7940  axpre-ltadd  7970  axpre-mulgt0  7971  axpre-mulext  7972  axarch  7975  nntopi  7978  axcaucvglemval  7981  axcaucvglemcau  7982  axcaucvglemres  7983  axpre-suploclemres  7985  ltaddneg  8468  ltsubadd2  8477  lesubadd2  8479  ltaddsub  8480  leaddsub  8482  ltaddpos2  8497  posdif  8499  lesub1  8500  ltsub1  8502  ltnegcon1  8507  lenegcon1  8510  addge02  8517  leaddle0  8521  ltordlem  8526  possumd  8613  sublt0d  8614  apreap  8631  prodgt02  8897  prodge02  8899  ltmulgt12  8909  lemulge12  8911  ltdivmul  8920  ledivmul  8921  ltdivmul2  8922  lt2mul2div  8923  ledivmul2  8924  ltrec  8927  ltrec1  8932  ltdiv23  8936  lediv23  8937  nnge1  9030  halfpos  9239  lt2halves  9244  addltmul  9245  avglt2  9248  avgle2  9250  nnrecl  9264  zltlem1  9400  difgtsumgt  9412  nn0le2is012  9425  gtndiv  9438  qapne  9730  nnledivrp  9858  xltnegi  9927  xltadd1  9968  xsubge0  9973  xposdif  9974  xlesubadd  9975  xleaddadd  9979  divelunit  10094  eluzgtdifelfzo  10290  qtri3or  10347  exbtwnzlemstep  10354  exbtwnzlemshrink  10355  exbtwnzlemex  10356  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2zlemshrink  10360  rebtwn2z  10361  flqlelt  10383  flqbi  10397  2tnp1ge0ge0  10408  q2submod  10494  frec2uzltd  10512  frec2uzlt2d  10513  frec2uzf1od  10515  monoord  10594  ser3mono  10596  ser3ge0  10645  expnbnd  10772  nn0ltexp2  10818  facwordi  10849  hashunlem  10913  zfz1isolemiso  10948  seq3coll  10951  caucvgrelemcau  11162  caucvgre  11163  cvg1nlemcau  11166  cvg1nlemres  11167  recvguniq  11177  resqrexlemover  11192  resqrexlemgt0  11202  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemsqa  11206  resqrexlemex  11207  maxleastlt  11397  minmax  11412  lemininf  11416  ltmininf  11417  xrmaxleastlt  11438  xrmaxltsup  11440  xrminmax  11447  xrmin1inf  11449  xrmin2inf  11450  xrltmininf  11452  xrlemininf  11453  climserle  11527  summodclem3  11562  summodclem2a  11563  summodc  11565  zsumdc  11566  fsum3  11569  fsum00  11644  fsumabs  11647  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  zproddc  11761  fprodseq  11765  fprodle  11822  sin01bnd  11939  cos01bnd  11940  summodnegmod  12004  modmulconst  12005  dvdsaddr  12019  dvdssub  12020  dvdssubr  12021  dvdslelemd  12025  dvdsfac  12042  dvdsmod  12044  oddp1even  12058  ltoddhalfle  12075  opoe  12077  omoe  12078  divalg2  12108  divalgmod  12109  ndvdssub  12112  ndvdsadd  12113  bitsfval  12124  bitsval  12125  bits0  12130  bitsp1  12133  bitsfzolem  12136  bitsfzo  12137  bitscmp  12140  bitsinv1lem  12143  bezoutlembi  12197  dvdssqim  12216  dvdsmulgcd  12217  dvdssq  12223  nn0seqcvgd  12234  coprmdvds  12285  coprmdvds2  12286  rpmul  12291  cncongr1  12296  divgcdodd  12336  isprm6  12340  prmdvdsexp  12341  prmdvdsexpr  12343  prmfac1  12345  oddpwdclemxy  12362  oddpwdclemodd  12365  sqpweven  12368  2sqpwodd  12369  sqne2sq  12370  hashdvds  12414  phiprmpw  12415  eulerthlemh  12424  prmdiv  12428  prmdiveq  12429  odzval  12435  odzcllem  12436  odzdvds  12439  pythagtriplem11  12468  pythagtriplem13  12470  pythagtrip  12477  pceulem  12488  pczndvds2  12512  pcdvdsb  12514  pc2dvds  12524  pcz  12526  pcprmpw2  12527  dvdsprmpweq  12529  dvdsprmpweqle  12531  difsqpwdvds  12532  pcmpt  12537  prmpwdvds  12549  pockthlem  12550  4sqlem11  12595  exmidunben  12668  nninfdclemlt  12693  mulgval  13328  dvdsrtr  13733  dvdsrmul1  13734  unitnegcl  13762  unitpropdg  13780  elrhmunit  13809  zndvds0  14282  znunit  14291  psmettri2  14648  ismet2  14674  xmettri2  14681  comet  14819  ivthinclemum  14955  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemdisj  14960  ivthinclemloc  14961  ivthinc  14963  ivthreinc  14965  limccl  14979  ellimc3apf  14980  sin0pilem2  15102  pilem3  15103  sincosq1sgn  15146  sincosq2sgn  15147  sincosq4sgn  15149  logltb  15194  logle1b  15212  loglt1b  15213  logbgt0b  15286  wilthlem1  15300  sgmval  15303  dvdsppwf1o  15309  perfect1  15318  lgslem1  15325  lgsval  15329  lgsdilem  15352  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  lgseisenlem1  15395  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem2  15407  m1lgs  15410  2lgslem1a1  15411  2lgslem1a  15413  2lgsoddprmlem2  15431  2lgsoddprmlem3  15436  2sqlem4  15443  2sqlem8a  15447