Theorem breq2d 4041

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  breqtrd  4055  sbcbr1g  4085  pofun  4343  csbfv12g  5592  isorel  5851  isocnv  5854  isotr  5859  caovordig  6084  caovordg  6086  caovord  6090  xporderlem  6284  th3qlem2  6692  phplem3g  6912  supsnti  7064  inflbti  7083  difinfinf  7160  enqdc1  7422  ltanqg  7460  ltmnqg  7461  archnqq  7477  prarloclemarch2  7479  prloc  7551  addnqprllem  7587  addlocprlemgt  7594  appdivnq  7623  mulnqprl  7628  1idprl  7650  ltexprlemloc  7667  caucvgprlemcanl  7704  cauappcvgprlemm  7705  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlemlim  7721  cauappcvgpr  7722  archrecnq  7723  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemcl  7736  caucvgprlemladdrl  7738  caucvgpr  7742  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnkeqj  7750  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  caucvgprprlem1  7769  caucvgprprlem2  7770  caucvgprpr  7772  ltposr  7823  ltasrg  7830  mulgt0sr  7838  mulextsr1lem  7840  mulextsr1  7841  prsrlt  7847  caucvgsrlemcl  7849  caucvgsrlemfv  7851  caucvgsrlembound  7854  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  caucvgsr  7862  map2psrprg  7865  pitonnlem2  7907  pitonn  7908  recidpipr  7916  axpre-ltadd  7946  axpre-mulgt0  7947  axpre-mulext  7948  axarch  7951  nntopi  7954  axcaucvglemval  7957  axcaucvglemcau  7958  axcaucvglemres  7959  axpre-suploclemres  7961  ltaddneg  8443  ltsubadd2  8452  lesubadd2  8454  ltaddsub  8455  leaddsub  8457  ltaddpos2  8472  posdif  8474  lesub1  8475  ltsub1  8477  ltnegcon1  8482  lenegcon1  8485  addge02  8492  leaddle0  8496  ltordlem  8501  possumd  8588  sublt0d  8589  apreap  8606  prodgt02  8872  prodge02  8874  ltmulgt12  8884  lemulge12  8886  ltdivmul  8895  ledivmul  8896  ltdivmul2  8897  lt2mul2div  8898  ledivmul2  8899  ltrec  8902  ltrec1  8907  ltdiv23  8911  lediv23  8912  nnge1  9005  halfpos  9213  lt2halves  9218  addltmul  9219  avglt2  9222  avgle2  9224  nnrecl  9238  zltlem1  9374  difgtsumgt  9386  nn0le2is012  9399  gtndiv  9412  qapne  9704  nnledivrp  9832  xltnegi  9901  xltadd1  9942  xsubge0  9947  xposdif  9948  xlesubadd  9949  xleaddadd  9953  divelunit  10068  eluzgtdifelfzo  10264  qtri3or  10310  exbtwnzlemstep  10316  exbtwnzlemshrink  10317  exbtwnzlemex  10318  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2zlemshrink  10322  rebtwn2z  10323  flqlelt  10345  flqbi  10359  2tnp1ge0ge0  10370  q2submod  10456  frec2uzltd  10474  frec2uzlt2d  10475  frec2uzf1od  10477  monoord  10556  ser3mono  10558  ser3ge0  10607  expnbnd  10734  nn0ltexp2  10780  facwordi  10811  hashunlem  10875  zfz1isolemiso  10910  seq3coll  10913  caucvgrelemcau  11124  caucvgre  11125  cvg1nlemcau  11128  cvg1nlemres  11129  recvguniq  11139  resqrexlemover  11154  resqrexlemgt0  11164  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemsqa  11168  resqrexlemex  11169  maxleastlt  11359  minmax  11373  lemininf  11377  ltmininf  11378  xrmaxleastlt  11399  xrmaxltsup  11401  xrminmax  11408  xrmin1inf  11410  xrmin2inf  11411  xrltmininf  11413  xrlemininf  11414  climserle  11488  summodclem3  11523  summodclem2a  11524  summodc  11526  zsumdc  11527  fsum3  11530  fsum00  11605  fsumabs  11608  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  zproddc  11722  fprodseq  11726  fprodle  11783  sin01bnd  11900  cos01bnd  11901  summodnegmod  11965  modmulconst  11966  dvdsaddr  11980  dvdssub  11981  dvdssubr  11982  dvdslelemd  11985  dvdsfac  12002  dvdsmod  12004  oddp1even  12017  ltoddhalfle  12034  opoe  12036  omoe  12037  divalg2  12067  divalgmod  12068  ndvdssub  12071  ndvdsadd  12072  bezoutlembi  12142  dvdssqim  12161  dvdsmulgcd  12162  dvdssq  12168  nn0seqcvgd  12179  coprmdvds  12230  coprmdvds2  12231  rpmul  12236  cncongr1  12241  divgcdodd  12281  isprm6  12285  prmdvdsexp  12286  prmdvdsexpr  12288  prmfac1  12290  oddpwdclemxy  12307  oddpwdclemodd  12310  sqpweven  12313  2sqpwodd  12314  sqne2sq  12315  hashdvds  12359  phiprmpw  12360  eulerthlemh  12369  prmdiv  12373  prmdiveq  12374  odzval  12379  odzcllem  12380  odzdvds  12383  pythagtriplem11  12412  pythagtriplem13  12414  pythagtrip  12421  pceulem  12432  pczndvds2  12456  pcdvdsb  12458  pc2dvds  12468  pcz  12470  pcprmpw2  12471  dvdsprmpweq  12473  dvdsprmpweqle  12475  difsqpwdvds  12476  pcmpt  12481  prmpwdvds  12493  pockthlem  12494  4sqlem11  12539  exmidunben  12583  nninfdclemlt  12608  mulgval  13192  dvdsrtr  13597  dvdsrmul1  13598  unitnegcl  13626  unitpropdg  13644  elrhmunit  13673  zndvds0  14138  znunit  14147  psmettri2  14496  ismet2  14522  xmettri2  14529  comet  14667  ivthinclemum  14789  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemdisj  14794  ivthinclemloc  14795  ivthinc  14797  ivthreinc  14799  limccl  14813  ellimc3apf  14814  sin0pilem2  14917  pilem3  14918  sincosq1sgn  14961  sincosq2sgn  14962  sincosq4sgn  14964  logltb  15009  logle1b  15027  loglt1b  15028  logbgt0b  15098  wilthlem1  15112  lgslem1  15116  lgsval  15120  lgsdilem  15143  lgsne0  15154  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  lgseisenlem1  15186  lgseisenlem2  15187  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem2  15194  2lgsoddprmlem3  15199  2sqlem4  15205  2sqlem8a  15209