Theorem breq2d 4142

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 4134	. 2 |- ( A = B -> ( C R A <-> C R B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C R A <-> C R B ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  breqtrd  4156  sbcbr1g  4187  pofun  4457  csbfv12g  5736  isorel  6014  isocnv  6017  isotr  6022  caovordig  6255  caovordg  6257  caovord  6261  xporderlem  6467  th3qlem2  6912  phplem3g  7157  supsnti  7345  inflbti  7364  difinfinf  7441  enqdc1  7729  ltanqg  7767  ltmnqg  7768  archnqq  7784  prarloclemarch2  7786  prloc  7858  addnqprllem  7894  addlocprlemgt  7901  appdivnq  7930  mulnqprl  7935  1idprl  7957  ltexprlemloc  7974  caucvgprlemcanl  8011  cauappcvgprlemm  8012  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  archrecnq  8030  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemcl  8043  caucvgprlemladdrl  8045  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgprpr  8079  ltposr  8130  ltasrg  8137  mulgt0sr  8145  mulextsr1lem  8147  mulextsr1  8148  prsrlt  8154  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsrlembound  8161  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  map2psrprg  8172  pitonnlem2  8214  pitonn  8215  recidpipr  8223  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  axarch  8258  nntopi  8261  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  ltaddneg  8752  ltsubadd2  8761  lesubadd2  8763  ltaddsub  8764  leaddsub  8766  ltaddpos2  8781  posdif  8783  lesub1  8784  ltsub1  8786  ltnegcon1  8791  lenegcon1  8794  addge02  8801  leaddle0  8805  ltordlem  8810  possumd  8898  sublt0d  8899  apreap  8916  prodgt02  9184  prodge02  9186  ltmulgt12  9196  lemulge12  9198  ltdivmul  9207  ledivmul  9208  ltdivmul2  9209  lt2mul2div  9210  ledivmul2  9211  ltrec  9214  ltrec1  9219  ltdiv23  9223  lediv23  9224  nnge1  9328  halfpos  9538  lt2halves  9543  addltmul  9544  avglt2  9547  avgle2  9549  nnrecl  9563  zltlem1  9704  difgtsumgt  9716  nn0le2is012  9730  gtndiv  9743  qapne  10041  nnledivrp  10169  xltnegi  10239  xltadd1  10280  xsubge0  10285  xposdif  10286  xlesubadd  10287  xleaddadd  10291  divelunit  10406  eluzgtdifelfzo  10617  qtri3or  10677  exbtwnzlemstep  10684  exbtwnzlemshrink  10685  exbtwnzlemex  10686  exbtwnz  10687  rebtwn2zlemstep  10689  rebtwn2zlemshrink  10690  rebtwn2z  10691  flqlelt  10713  flqbi  10727  2tnp1ge0ge0  10738  q2submod  10824  frec2uzltd  10842  frec2uzlt2d  10843  frec2uzf1od  10845  monoord  10924  ser3mono  10926  ser3ge0  10975  expnbnd  11103  nn0ltexp2  11149  facwordi  11180  hashunlem  11246  ssenneg  11282  zfz1isolemiso  11293  seq3coll  11296  swrdccat3blem  11513  caucvgrelemcau  11748  caucvgre  11749  cvg1nlemcau  11752  cvg1nlemres  11753  recvguniq  11763  resqrexlemover  11778  resqrexlemgt0  11788  resqrexlemoverl  11789  resqrexlemglsq  11790  resqrexlemsqa  11792  resqrexlemex  11793  maxleastlt  11983  minmax  11998  lemininf  12002  ltmininf  12003  xrmaxleastlt  12024  xrmaxltsup  12026  xrminmax  12033  xrmin1inf  12035  xrmin2inf  12036  xrltmininf  12038  xrlemininf  12039  climserle  12113  summodclem3  12149  summodclem2a  12150  summodc  12152  zsumdc  12153  fsum3  12156  fsum00  12231  fsumabs  12234  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  zproddc  12348  fprodseq  12352  fprodle  12409  sin01bnd  12526  cos01bnd  12527  summodnegmod  12591  modmulconst  12592  dvdsaddr  12606  dvdssub  12607  dvdssubr  12608  dvdslelemd  12612  dvdsfac  12629  dvdsmod  12631  oddp1even  12645  ltoddhalfle  12662  opoe  12664  omoe  12665  divalg2  12695  divalgmod  12696  ndvdssub  12699  ndvdsadd  12700  bitsfval  12711  bitsval  12712  bits0  12717  bitsp1  12720  bitsfzolem  12723  bitsfzo  12724  bitscmp  12727  bitsinv1lem  12730  bezoutlembi  12784  dvdssqim  12803  dvdsmulgcd  12804  dvdssq  12810  nn0seqcvgd  12821  coprmdvds  12872  coprmdvds2  12873  rpmul  12878  cncongr1  12883  divgcdodd  12923  isprm6  12927  prmdvdsexp  12928  prmdvdsexpr  12930  prmfac1  12932  oddpwdclemxy  12949  oddpwdclemodd  12952  sqpweven  12955  2sqpwodd  12956  sqne2sq  12957  hashdvds  13001  phiprmpw  13002  eulerthlemh  13011  prmdiv  13015  prmdiveq  13016  odzval  13022  odzcllem  13023  odzdvds  13026  pythagtriplem11  13055  pythagtriplem13  13057  pythagtrip  13064  pceulem  13075  pczndvds2  13099  pcdvdsb  13101  pc2dvds  13111  pcz  13113  pcprmpw2  13114  dvdsprmpweq  13116  dvdsprmpweqle  13118  difsqpwdvds  13119  pcmpt  13124  prmpwdvds  13136  pockthlem  13137  4sqlem11  13182  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfileme  13238  ballotfilemefi  13239  ballotfilemodife  13242  ballotfilem4  13243  ballotfilem1c  13253  ballotfilemsval  13254  ballotfilemieq  13262  ballotfilemfrcn0  13275  ballotfi  13284  exmidunben  13319  nninfdclemlt  13344  mulgval  13927  dvdsrtr  14410  dvdsrmul1  14411  unitnegcl  14439  unitpropdg  14457  elrhmunit  14486  zndvds0  14987  znunit  14996  mplsubgfilemcl  15092  psmettri2  15431  ismet2  15457  xmettri2  15464  comet  15602  ivthinclemum  15738  ivthinclemlopn  15739  ivthinclemlr  15740  ivthinclemuopn  15741  ivthinclemur  15742  ivthinclemdisj  15743  ivthinclemloc  15744  ivthinc  15746  ivthreinc  15748  limccl  15762  ellimc3apf  15763  sin0pilem2  15886  pilem3  15887  sincosq1sgn  15930  sincosq2sgn  15931  sincosq4sgn  15933  logltb  15979  logle1b  15997  loglt1b  15998  logbgt0b  16074  wilthlem1  16100  sgmval  16103  dvdsppwf1o  16109  perfect1  16118  bcmono  16124  bclbnd  16127  lgslem1  16131  lgsval  16135  lgsdilem  16158  lgsne0  16169  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  lgseisenlem1  16201  lgseisenlem2  16202  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad2lem2  16213  m1lgs  16216  2lgslem1a1  16217  2lgslem1a  16219  2lgsoddprmlem2  16237  2lgsoddprmlem3  16242  2sqlem4  16249  2sqlem8a  16253  eupth2lem3lem3fi  16723  eupth2lem3lem6fi  16724  eupth2lem3lem4fi  16726  eupth2lem3lem7fi  16727  eupth2lemsfi  16731  eupth2fi  16732  konigsberglem4  16744