Theorem breq2d 4017

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
breq2d	|- ( ph -> ( C R A <-> C R B ) )

Proof of Theorem breq2d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- ( ph -> A = B )
2		breq2 4009	. 2 |- ( A = B -> ( C R A <-> C R B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C R A <-> C R B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   class class class wbr 4005

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  breqtrd  4031  sbcbr1g  4061  pofun  4314  csbfv12g  5553  isorel  5811  isocnv  5814  isotr  5819  caovordig  6042  caovordg  6044  caovord  6048  xporderlem  6234  th3qlem2  6640  phplem3g  6858  supsnti  7006  inflbti  7025  difinfinf  7102  enqdc1  7363  ltanqg  7401  ltmnqg  7402  archnqq  7418  prarloclemarch2  7420  prloc  7492  addnqprllem  7528  addlocprlemgt  7535  appdivnq  7564  mulnqprl  7569  1idprl  7591  ltexprlemloc  7608  caucvgprlemcanl  7645  cauappcvgprlemm  7646  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem1  7660  cauappcvgprlemlim  7662  cauappcvgpr  7663  archrecnq  7664  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemm  7669  caucvgprlemcl  7677  caucvgprlemladdrl  7679  caucvgpr  7683  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemnkeqj  7691  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemloc  7704  caucvgprprlemclphr  7706  caucvgprprlemexbt  7707  caucvgprprlem1  7710  caucvgprprlem2  7711  caucvgprpr  7713  ltposr  7764  ltasrg  7771  mulgt0sr  7779  mulextsr1lem  7781  mulextsr1  7782  prsrlt  7788  caucvgsrlemcl  7790  caucvgsrlemfv  7792  caucvgsrlembound  7795  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  caucvgsr  7803  map2psrprg  7806  pitonnlem2  7848  pitonn  7849  recidpipr  7857  axpre-ltadd  7887  axpre-mulgt0  7888  axpre-mulext  7889  axarch  7892  nntopi  7895  axcaucvglemval  7898  axcaucvglemcau  7899  axcaucvglemres  7900  axpre-suploclemres  7902  ltaddneg  8383  ltsubadd2  8392  lesubadd2  8394  ltaddsub  8395  leaddsub  8397  ltaddpos2  8412  posdif  8414  lesub1  8415  ltsub1  8417  ltnegcon1  8422  lenegcon1  8425  addge02  8432  leaddle0  8436  ltordlem  8441  possumd  8528  sublt0d  8529  apreap  8546  prodgt02  8812  prodge02  8814  ltmulgt12  8824  lemulge12  8826  ltdivmul  8835  ledivmul  8836  ltdivmul2  8837  lt2mul2div  8838  ledivmul2  8839  ltrec  8842  ltrec1  8847  ltdiv23  8851  lediv23  8852  nnge1  8944  halfpos  9152  lt2halves  9156  addltmul  9157  avglt2  9160  avgle2  9162  nnrecl  9176  zltlem1  9312  difgtsumgt  9324  nn0le2is012  9337  gtndiv  9350  qapne  9641  nnledivrp  9768  xltnegi  9837  xltadd1  9878  xsubge0  9883  xposdif  9884  xlesubadd  9885  xleaddadd  9889  divelunit  10004  eluzgtdifelfzo  10199  qtri3or  10245  exbtwnzlemstep  10250  exbtwnzlemshrink  10251  exbtwnzlemex  10252  exbtwnz  10253  rebtwn2zlemstep  10255  rebtwn2zlemshrink  10256  rebtwn2z  10257  flqlelt  10278  flqbi  10292  2tnp1ge0ge0  10303  q2submod  10387  frec2uzltd  10405  frec2uzlt2d  10406  frec2uzf1od  10408  monoord  10478  ser3mono  10480  ser3ge0  10519  expnbnd  10646  nn0ltexp2  10691  facwordi  10722  hashunlem  10786  zfz1isolemiso  10821  seq3coll  10824  caucvgrelemcau  10991  caucvgre  10992  cvg1nlemcau  10995  cvg1nlemres  10996  recvguniq  11006  resqrexlemover  11021  resqrexlemgt0  11031  resqrexlemoverl  11032  resqrexlemglsq  11033  resqrexlemsqa  11035  resqrexlemex  11036  maxleastlt  11226  minmax  11240  lemininf  11244  ltmininf  11245  xrmaxleastlt  11266  xrmaxltsup  11268  xrminmax  11275  xrmin1inf  11277  xrmin2inf  11278  xrltmininf  11280  xrlemininf  11281  climserle  11355  summodclem3  11390  summodclem2a  11391  summodc  11393  zsumdc  11394  fsum3  11397  fsum00  11472  fsumabs  11475  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  zproddc  11589  fprodseq  11593  fprodle  11650  sin01bnd  11767  cos01bnd  11768  summodnegmod  11831  modmulconst  11832  dvdsaddr  11846  dvdssub  11847  dvdssubr  11848  dvdslelemd  11851  dvdsfac  11868  dvdsmod  11870  oddp1even  11883  ltoddhalfle  11900  opoe  11902  omoe  11903  divalg2  11933  divalgmod  11934  ndvdssub  11937  ndvdsadd  11938  bezoutlembi  12008  dvdssqim  12027  dvdsmulgcd  12028  dvdssq  12034  nn0seqcvgd  12043  coprmdvds  12094  coprmdvds2  12095  rpmul  12100  cncongr1  12105  divgcdodd  12145  isprm6  12149  prmdvdsexp  12150  prmdvdsexpr  12152  prmfac1  12154  oddpwdclemxy  12171  oddpwdclemodd  12174  sqpweven  12177  2sqpwodd  12178  sqne2sq  12179  hashdvds  12223  phiprmpw  12224  eulerthlemh  12233  prmdiv  12237  prmdiveq  12238  odzval  12243  odzcllem  12244  odzdvds  12247  pythagtriplem11  12276  pythagtriplem13  12278  pythagtrip  12285  pceulem  12296  pczndvds2  12319  pcdvdsb  12321  pc2dvds  12331  pcz  12333  pcprmpw2  12334  dvdsprmpweq  12336  dvdsprmpweqle  12338  difsqpwdvds  12339  pcmpt  12343  prmpwdvds  12355  pockthlem  12356  exmidunben  12429  nninfdclemlt  12454  mulgval  12991  dvdsrtr  13275  dvdsrmul1  13276  unitnegcl  13304  unitpropdg  13322  psmettri2  13867  ismet2  13893  xmettri2  13900  comet  14038  ivthinclemum  14152  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemdisj  14157  ivthinclemloc  14158  ivthinc  14160  limccl  14167  ellimc3apf  14168  sin0pilem2  14242  pilem3  14243  sincosq1sgn  14286  sincosq2sgn  14287  sincosq4sgn  14289  logltb  14334  logle1b  14352  loglt1b  14353  logbgt0b  14423  lgslem1  14440  lgsval  14444  lgsdilem  14467  lgsne0  14478  lgseisenlem1  14489  lgseisenlem2  14490  m1lgs  14491  2lgsoddprmlem2  14493  2lgsoddprmlem3  14498  2sqlem4  14504  2sqlem8a  14508