Theorem breq2d 3977

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 3969	. 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 104   = wceq 1335   class class class wbr 3965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567  df-op 3569  df-br 3966

This theorem is referenced by:  breqtrd  3990  sbcbr1g  4020  pofun  4272  csbfv12g  5503  isorel  5755  isocnv  5758  isotr  5763  caovordig  5983  caovordg  5985  caovord  5989  xporderlem  6175  th3qlem2  6580  phplem3g  6798  supsnti  6945  inflbti  6964  difinfinf  7039  enqdc1  7276  ltanqg  7314  ltmnqg  7315  archnqq  7331  prarloclemarch2  7333  prloc  7405  addnqprllem  7441  addlocprlemgt  7448  appdivnq  7477  mulnqprl  7482  1idprl  7504  ltexprlemloc  7521  caucvgprlemcanl  7558  cauappcvgprlemm  7559  cauappcvgprlemladdru  7570  cauappcvgprlemladdrl  7571  cauappcvgprlem1  7573  cauappcvgprlemlim  7575  cauappcvgpr  7576  archrecnq  7577  caucvgprlemnkj  7580  caucvgprlemnbj  7581  caucvgprlemm  7582  caucvgprlemcl  7590  caucvgprlemladdrl  7592  caucvgpr  7596  caucvgprprlemell  7599  caucvgprprlemelu  7600  caucvgprprlemcbv  7601  caucvgprprlemval  7602  caucvgprprlemnkeqj  7604  caucvgprprlemml  7608  caucvgprprlemmu  7609  caucvgprprlemopl  7611  caucvgprprlemlol  7612  caucvgprprlemopu  7613  caucvgprprlemloc  7617  caucvgprprlemclphr  7619  caucvgprprlemexbt  7620  caucvgprprlem1  7623  caucvgprprlem2  7624  caucvgprpr  7626  ltposr  7677  ltasrg  7684  mulgt0sr  7692  mulextsr1lem  7694  mulextsr1  7695  prsrlt  7701  caucvgsrlemcl  7703  caucvgsrlemfv  7705  caucvgsrlembound  7708  caucvgsrlemgt1  7709  caucvgsrlemoffres  7714  caucvgsr  7716  map2psrprg  7719  pitonnlem2  7761  pitonn  7762  recidpipr  7770  axpre-ltadd  7800  axpre-mulgt0  7801  axpre-mulext  7802  axarch  7805  nntopi  7808  axcaucvglemval  7811  axcaucvglemcau  7812  axcaucvglemres  7813  axpre-suploclemres  7815  ltaddneg  8293  ltsubadd2  8302  lesubadd2  8304  ltaddsub  8305  leaddsub  8307  ltaddpos2  8322  posdif  8324  lesub1  8325  ltsub1  8327  ltnegcon1  8332  lenegcon1  8335  addge02  8342  leaddle0  8346  ltordlem  8351  possumd  8438  sublt0d  8439  apreap  8456  prodgt02  8718  prodge02  8720  ltmulgt12  8730  lemulge12  8732  ltdivmul  8741  ledivmul  8742  ltdivmul2  8743  lt2mul2div  8744  ledivmul2  8745  ltrec  8748  ltrec1  8753  ltdiv23  8757  lediv23  8758  nnge1  8850  halfpos  9058  lt2halves  9062  addltmul  9063  avglt2  9066  avgle2  9068  nnrecl  9082  zltlem1  9218  nn0le2is012  9240  gtndiv  9253  qapne  9541  nnledivrp  9666  xltnegi  9732  xltadd1  9773  xsubge0  9778  xposdif  9779  xlesubadd  9780  xleaddadd  9784  divelunit  9899  eluzgtdifelfzo  10089  qtri3or  10135  exbtwnzlemstep  10140  exbtwnzlemshrink  10141  exbtwnzlemex  10142  exbtwnz  10143  rebtwn2zlemstep  10145  rebtwn2zlemshrink  10146  rebtwn2z  10147  flqlelt  10168  flqbi  10182  2tnp1ge0ge0  10193  q2submod  10277  frec2uzltd  10295  frec2uzlt2d  10296  frec2uzf1od  10298  monoord  10368  ser3mono  10370  ser3ge0  10409  expnbnd  10534  facwordi  10607  hashunlem  10671  zfz1isolemiso  10703  seq3coll  10706  caucvgrelemcau  10873  caucvgre  10874  cvg1nlemcau  10877  cvg1nlemres  10878  recvguniq  10888  resqrexlemover  10903  resqrexlemgt0  10913  resqrexlemoverl  10914  resqrexlemglsq  10915  resqrexlemsqa  10917  resqrexlemex  10918  maxleastlt  11108  minmax  11122  lemininf  11126  ltmininf  11127  xrmaxleastlt  11146  xrmaxltsup  11148  xrminmax  11155  xrmin1inf  11157  xrmin2inf  11158  xrltmininf  11160  xrlemininf  11161  climserle  11235  summodclem3  11270  summodclem2a  11271  summodc  11273  zsumdc  11274  fsum3  11277  fsum00  11352  fsumabs  11355  cvgratnnlemnexp  11414  cvgratnnlemmn  11415  zproddc  11469  fprodseq  11473  fprodle  11530  sin01bnd  11647  cos01bnd  11648  summodnegmod  11710  modmulconst  11711  dvdsaddr  11723  dvdssub  11724  dvdssubr  11725  dvdslelemd  11727  dvdsfac  11744  dvdsmod  11746  oddp1even  11759  ltoddhalfle  11776  opoe  11778  omoe  11779  divalg2  11809  divalgmod  11810  ndvdssub  11813  ndvdsadd  11814  bezoutlembi  11880  dvdssqim  11899  dvdsmulgcd  11900  dvdssq  11906  nn0seqcvgd  11909  coprmdvds  11960  coprmdvds2  11961  rpmul  11966  cncongr1  11971  divgcdodd  12008  isprm6  12012  prmdvdsexp  12013  prmdvdsexpr  12015  prmfac1  12017  oddpwdclemxy  12034  oddpwdclemodd  12037  sqpweven  12040  2sqpwodd  12041  sqne2sq  12042  hashdvds  12084  phiprmpw  12085  eulerthlemh  12094  prmdiv  12098  prmdiveq  12099  exmidunben  12138  psmettri2  12699  ismet2  12725  xmettri2  12732  comet  12870  ivthinclemum  12984  ivthinclemlopn  12985  ivthinclemlr  12986  ivthinclemuopn  12987  ivthinclemur  12988  ivthinclemdisj  12989  ivthinclemloc  12990  ivthinc  12992  limccl  12999  ellimc3apf  13000  sin0pilem2  13074  pilem3  13075  sincosq1sgn  13118  sincosq2sgn  13119  sincosq4sgn  13121  logltb  13166  logle1b  13184  loglt1b  13185  logbgt0b  13254