Theorem breq2d 4105

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  breqtrd  4119  sbcbr1g  4150  pofun  4415  csbfv12g  5688  isorel  5959  isocnv  5962  isotr  5967  caovordig  6198  caovordg  6200  caovord  6204  xporderlem  6405  th3qlem2  6850  phplem3g  7085  supsnti  7247  inflbti  7266  difinfinf  7343  enqdc1  7625  ltanqg  7663  ltmnqg  7664  archnqq  7680  prarloclemarch2  7682  prloc  7754  addnqprllem  7790  addlocprlemgt  7797  appdivnq  7826  mulnqprl  7831  1idprl  7853  ltexprlemloc  7870  caucvgprlemcanl  7907  cauappcvgprlemm  7908  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlemlim  7924  cauappcvgpr  7925  archrecnq  7926  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemcl  7939  caucvgprlemladdrl  7941  caucvgpr  7945  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemnkeqj  7953  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  caucvgprprlem1  7972  caucvgprprlem2  7973  caucvgprpr  7975  ltposr  8026  ltasrg  8033  mulgt0sr  8041  mulextsr1lem  8043  mulextsr1  8044  prsrlt  8050  caucvgsrlemcl  8052  caucvgsrlemfv  8054  caucvgsrlembound  8057  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  caucvgsr  8065  map2psrprg  8068  pitonnlem2  8110  pitonn  8111  recidpipr  8119  axpre-ltadd  8149  axpre-mulgt0  8150  axpre-mulext  8151  axarch  8154  nntopi  8157  axcaucvglemval  8160  axcaucvglemcau  8161  axcaucvglemres  8162  axpre-suploclemres  8164  ltaddneg  8646  ltsubadd2  8655  lesubadd2  8657  ltaddsub  8658  leaddsub  8660  ltaddpos2  8675  posdif  8677  lesub1  8678  ltsub1  8680  ltnegcon1  8685  lenegcon1  8688  addge02  8695  leaddle0  8699  ltordlem  8704  possumd  8791  sublt0d  8792  apreap  8809  prodgt02  9075  prodge02  9077  ltmulgt12  9087  lemulge12  9089  ltdivmul  9098  ledivmul  9099  ltdivmul2  9100  lt2mul2div  9101  ledivmul2  9102  ltrec  9105  ltrec1  9110  ltdiv23  9114  lediv23  9115  nnge1  9208  halfpos  9417  lt2halves  9422  addltmul  9423  avglt2  9426  avgle2  9428  nnrecl  9442  zltlem1  9581  difgtsumgt  9593  nn0le2is012  9606  gtndiv  9619  qapne  9917  nnledivrp  10045  xltnegi  10114  xltadd1  10155  xsubge0  10160  xposdif  10161  xlesubadd  10162  xleaddadd  10166  divelunit  10281  eluzgtdifelfzo  10488  qtri3or  10546  exbtwnzlemstep  10553  exbtwnzlemshrink  10554  exbtwnzlemex  10555  exbtwnz  10556  rebtwn2zlemstep  10558  rebtwn2zlemshrink  10559  rebtwn2z  10560  flqlelt  10582  flqbi  10596  2tnp1ge0ge0  10607  q2submod  10693  frec2uzltd  10711  frec2uzlt2d  10712  frec2uzf1od  10714  monoord  10793  ser3mono  10795  ser3ge0  10844  expnbnd  10971  nn0ltexp2  11017  facwordi  11048  hashunlem  11113  zfz1isolemiso  11149  seq3coll  11152  swrdccat3blem  11369  caucvgrelemcau  11603  caucvgre  11604  cvg1nlemcau  11607  cvg1nlemres  11608  recvguniq  11618  resqrexlemover  11633  resqrexlemgt0  11643  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemsqa  11647  resqrexlemex  11648  maxleastlt  11838  minmax  11853  lemininf  11857  ltmininf  11858  xrmaxleastlt  11879  xrmaxltsup  11881  xrminmax  11888  xrmin1inf  11890  xrmin2inf  11891  xrltmininf  11893  xrlemininf  11894  climserle  11968  summodclem3  12004  summodclem2a  12005  summodc  12007  zsumdc  12008  fsum3  12011  fsum00  12086  fsumabs  12089  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  zproddc  12203  fprodseq  12207  fprodle  12264  sin01bnd  12381  cos01bnd  12382  summodnegmod  12446  modmulconst  12447  dvdsaddr  12461  dvdssub  12462  dvdssubr  12463  dvdslelemd  12467  dvdsfac  12484  dvdsmod  12486  oddp1even  12500  ltoddhalfle  12517  opoe  12519  omoe  12520  divalg2  12550  divalgmod  12551  ndvdssub  12554  ndvdsadd  12555  bitsfval  12566  bitsval  12567  bits0  12572  bitsp1  12575  bitsfzolem  12578  bitsfzo  12579  bitscmp  12582  bitsinv1lem  12585  bezoutlembi  12639  dvdssqim  12658  dvdsmulgcd  12659  dvdssq  12665  nn0seqcvgd  12676  coprmdvds  12727  coprmdvds2  12728  rpmul  12733  cncongr1  12738  divgcdodd  12778  isprm6  12782  prmdvdsexp  12783  prmdvdsexpr  12785  prmfac1  12787  oddpwdclemxy  12804  oddpwdclemodd  12807  sqpweven  12810  2sqpwodd  12811  sqne2sq  12812  hashdvds  12856  phiprmpw  12857  eulerthlemh  12866  prmdiv  12870  prmdiveq  12871  odzval  12877  odzcllem  12878  odzdvds  12881  pythagtriplem11  12910  pythagtriplem13  12912  pythagtrip  12919  pceulem  12930  pczndvds2  12954  pcdvdsb  12956  pc2dvds  12966  pcz  12968  pcprmpw2  12969  dvdsprmpweq  12971  dvdsprmpweqle  12973  difsqpwdvds  12974  pcmpt  12979  prmpwdvds  12991  pockthlem  12992  4sqlem11  13037  exmidunben  13110  nninfdclemlt  13135  mulgval  13772  dvdsrtr  14179  dvdsrmul1  14180  unitnegcl  14208  unitpropdg  14226  elrhmunit  14255  zndvds0  14729  znunit  14738  mplsubgfilemcl  14783  psmettri2  15122  ismet2  15148  xmettri2  15155  comet  15293  ivthinclemum  15429  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemdisj  15434  ivthinclemloc  15435  ivthinc  15437  ivthreinc  15439  limccl  15453  ellimc3apf  15454  sin0pilem2  15576  pilem3  15577  sincosq1sgn  15620  sincosq2sgn  15621  sincosq4sgn  15623  logltb  15668  logle1b  15686  loglt1b  15687  logbgt0b  15760  wilthlem1  15777  sgmval  15780  dvdsppwf1o  15786  perfect1  15795  lgslem1  15802  lgsval  15806  lgsdilem  15829  lgsne0  15840  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  lgseisenlem1  15872  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem2  15884  m1lgs  15887  2lgslem1a1  15888  2lgslem1a  15890  2lgsoddprmlem2  15908  2lgsoddprmlem3  15913  2sqlem4  15920  2sqlem8a  15924  eupth2lem3lem3fi  16394  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397  eupth2lem3lem7fi  16398  eupth2lemsfi  16402  eupth2fi  16403  konigsberglem4  16415