Theorem breq2d 3993

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 3985	. 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 1343   class class class wbr 3981

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982

This theorem is referenced by:  breqtrd  4007  sbcbr1g  4037  pofun  4289  csbfv12g  5521  isorel  5775  isocnv  5778  isotr  5783  caovordig  6003  caovordg  6005  caovord  6009  xporderlem  6195  th3qlem2  6600  phplem3g  6818  supsnti  6966  inflbti  6985  difinfinf  7062  enqdc1  7299  ltanqg  7337  ltmnqg  7338  archnqq  7354  prarloclemarch2  7356  prloc  7428  addnqprllem  7464  addlocprlemgt  7471  appdivnq  7500  mulnqprl  7505  1idprl  7527  ltexprlemloc  7544  caucvgprlemcanl  7581  cauappcvgprlemm  7582  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlemlim  7598  cauappcvgpr  7599  archrecnq  7600  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemcl  7613  caucvgprlemladdrl  7615  caucvgpr  7619  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemnkeqj  7627  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemopu  7636  caucvgprprlemloc  7640  caucvgprprlemclphr  7642  caucvgprprlemexbt  7643  caucvgprprlem1  7646  caucvgprprlem2  7647  caucvgprpr  7649  ltposr  7700  ltasrg  7707  mulgt0sr  7715  mulextsr1lem  7717  mulextsr1  7718  prsrlt  7724  caucvgsrlemcl  7726  caucvgsrlemfv  7728  caucvgsrlembound  7731  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  caucvgsr  7739  map2psrprg  7742  pitonnlem2  7784  pitonn  7785  recidpipr  7793  axpre-ltadd  7823  axpre-mulgt0  7824  axpre-mulext  7825  axarch  7828  nntopi  7831  axcaucvglemval  7834  axcaucvglemcau  7835  axcaucvglemres  7836  axpre-suploclemres  7838  ltaddneg  8318  ltsubadd2  8327  lesubadd2  8329  ltaddsub  8330  leaddsub  8332  ltaddpos2  8347  posdif  8349  lesub1  8350  ltsub1  8352  ltnegcon1  8357  lenegcon1  8360  addge02  8367  leaddle0  8371  ltordlem  8376  possumd  8463  sublt0d  8464  apreap  8481  prodgt02  8744  prodge02  8746  ltmulgt12  8756  lemulge12  8758  ltdivmul  8767  ledivmul  8768  ltdivmul2  8769  lt2mul2div  8770  ledivmul2  8771  ltrec  8774  ltrec1  8779  ltdiv23  8783  lediv23  8784  nnge1  8876  halfpos  9084  lt2halves  9088  addltmul  9089  avglt2  9092  avgle2  9094  nnrecl  9108  zltlem1  9244  difgtsumgt  9256  nn0le2is012  9269  gtndiv  9282  qapne  9573  nnledivrp  9698  xltnegi  9767  xltadd1  9808  xsubge0  9813  xposdif  9814  xlesubadd  9815  xleaddadd  9819  divelunit  9934  eluzgtdifelfzo  10128  qtri3or  10174  exbtwnzlemstep  10179  exbtwnzlemshrink  10180  exbtwnzlemex  10181  exbtwnz  10182  rebtwn2zlemstep  10184  rebtwn2zlemshrink  10185  rebtwn2z  10186  flqlelt  10207  flqbi  10221  2tnp1ge0ge0  10232  q2submod  10316  frec2uzltd  10334  frec2uzlt2d  10335  frec2uzf1od  10337  monoord  10407  ser3mono  10409  ser3ge0  10448  expnbnd  10574  nn0ltexp2  10619  facwordi  10649  hashunlem  10713  zfz1isolemiso  10748  seq3coll  10751  caucvgrelemcau  10918  caucvgre  10919  cvg1nlemcau  10922  cvg1nlemres  10923  recvguniq  10933  resqrexlemover  10948  resqrexlemgt0  10958  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemsqa  10962  resqrexlemex  10963  maxleastlt  11153  minmax  11167  lemininf  11171  ltmininf  11172  xrmaxleastlt  11193  xrmaxltsup  11195  xrminmax  11202  xrmin1inf  11204  xrmin2inf  11205  xrltmininf  11207  xrlemininf  11208  climserle  11282  summodclem3  11317  summodclem2a  11318  summodc  11320  zsumdc  11321  fsum3  11324  fsum00  11399  fsumabs  11402  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  zproddc  11516  fprodseq  11520  fprodle  11577  sin01bnd  11694  cos01bnd  11695  summodnegmod  11758  modmulconst  11759  dvdsaddr  11773  dvdssub  11774  dvdssubr  11775  dvdslelemd  11777  dvdsfac  11794  dvdsmod  11796  oddp1even  11809  ltoddhalfle  11826  opoe  11828  omoe  11829  divalg2  11859  divalgmod  11860  ndvdssub  11863  ndvdsadd  11864  bezoutlembi  11934  dvdssqim  11953  dvdsmulgcd  11954  dvdssq  11960  nn0seqcvgd  11969  coprmdvds  12020  coprmdvds2  12021  rpmul  12026  cncongr1  12031  divgcdodd  12071  isprm6  12075  prmdvdsexp  12076  prmdvdsexpr  12078  prmfac1  12080  oddpwdclemxy  12097  oddpwdclemodd  12100  sqpweven  12103  2sqpwodd  12104  sqne2sq  12105  hashdvds  12149  phiprmpw  12150  eulerthlemh  12159  prmdiv  12163  prmdiveq  12164  odzval  12169  odzcllem  12170  odzdvds  12173  pythagtriplem11  12202  pythagtriplem13  12204  pythagtrip  12211  pceulem  12222  pczndvds2  12245  pcdvdsb  12247  pc2dvds  12257  pcz  12259  pcprmpw2  12260  dvdsprmpweq  12262  dvdsprmpweqle  12264  difsqpwdvds  12265  pcmpt  12269  prmpwdvds  12281  pockthlem  12282  exmidunben  12355  nninfdclemlt  12380  psmettri2  12928  ismet2  12954  xmettri2  12961  comet  13099  ivthinclemum  13213  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemdisj  13218  ivthinclemloc  13219  ivthinc  13221  limccl  13228  ellimc3apf  13229  sin0pilem2  13303  pilem3  13304  sincosq1sgn  13347  sincosq2sgn  13348  sincosq4sgn  13350  logltb  13395  logle1b  13413  loglt1b  13414  logbgt0b  13484  lgslem1  13501  lgsval  13505  lgsdilem  13528  lgsne0  13539  2sqlem4  13554  2sqlem8a  13558