Theorem breq2d 4140

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 4132	. 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 1402   class class class wbr 4128

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 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 theorem 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 3714  df-pr 3715  df-op 3717  df-br 4129

This theorem is referenced by:  breqtrd  4154  sbcbr1g  4185  pofun  4455  csbfv12g  5733  isorel  6008  isocnv  6011  isotr  6016  caovordig  6249  caovordg  6251  caovord  6255  xporderlem  6461  th3qlem2  6906  phplem3g  7151  supsnti  7339  inflbti  7358  difinfinf  7435  enqdc1  7723  ltanqg  7761  ltmnqg  7762  archnqq  7778  prarloclemarch2  7780  prloc  7852  addnqprllem  7888  addlocprlemgt  7895  appdivnq  7924  mulnqprl  7929  1idprl  7951  ltexprlemloc  7968  caucvgprlemcanl  8005  cauappcvgprlemm  8006  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  cauappcvgprlem1  8020  cauappcvgprlemlim  8022  cauappcvgpr  8023  archrecnq  8024  caucvgprlemnkj  8027  caucvgprlemnbj  8028  caucvgprlemm  8029  caucvgprlemcl  8037  caucvgprlemladdrl  8039  caucvgpr  8043  caucvgprprlemell  8046  caucvgprprlemelu  8047  caucvgprprlemcbv  8048  caucvgprprlemval  8049  caucvgprprlemnkeqj  8051  caucvgprprlemml  8055  caucvgprprlemmu  8056  caucvgprprlemopl  8058  caucvgprprlemlol  8059  caucvgprprlemopu  8060  caucvgprprlemloc  8064  caucvgprprlemclphr  8066  caucvgprprlemexbt  8067  caucvgprprlem1  8070  caucvgprprlem2  8071  caucvgprpr  8073  ltposr  8124  ltasrg  8131  mulgt0sr  8139  mulextsr1lem  8141  mulextsr1  8142  prsrlt  8148  caucvgsrlemcl  8150  caucvgsrlemfv  8152  caucvgsrlembound  8155  caucvgsrlemgt1  8156  caucvgsrlemoffres  8161  caucvgsr  8163  map2psrprg  8166  pitonnlem2  8208  pitonn  8209  recidpipr  8217  axpre-ltadd  8247  axpre-mulgt0  8248  axpre-mulext  8249  axarch  8252  nntopi  8255  axcaucvglemval  8258  axcaucvglemcau  8259  axcaucvglemres  8260  axpre-suploclemres  8262  ltaddneg  8746  ltsubadd2  8755  lesubadd2  8757  ltaddsub  8758  leaddsub  8760  ltaddpos2  8775  posdif  8777  lesub1  8778  ltsub1  8780  ltnegcon1  8785  lenegcon1  8788  addge02  8795  leaddle0  8799  ltordlem  8804  possumd  8891  sublt0d  8892  apreap  8909  prodgt02  9177  prodge02  9179  ltmulgt12  9189  lemulge12  9191  ltdivmul  9200  ledivmul  9201  ltdivmul2  9202  lt2mul2div  9203  ledivmul2  9204  ltrec  9207  ltrec1  9212  ltdiv23  9216  lediv23  9217  nnge1  9310  halfpos  9519  lt2halves  9524  addltmul  9525  avglt2  9528  avgle2  9530  nnrecl  9544  zltlem1  9685  difgtsumgt  9697  nn0le2is012  9711  gtndiv  9724  qapne  10022  nnledivrp  10150  xltnegi  10220  xltadd1  10261  xsubge0  10266  xposdif  10267  xlesubadd  10268  xleaddadd  10272  divelunit  10387  eluzgtdifelfzo  10598  qtri3or  10658  exbtwnzlemstep  10665  exbtwnzlemshrink  10666  exbtwnzlemex  10667  exbtwnz  10668  rebtwn2zlemstep  10670  rebtwn2zlemshrink  10671  rebtwn2z  10672  flqlelt  10694  flqbi  10708  2tnp1ge0ge0  10719  q2submod  10805  frec2uzltd  10823  frec2uzlt2d  10824  frec2uzf1od  10826  monoord  10905  ser3mono  10907  ser3ge0  10956  expnbnd  11084  nn0ltexp2  11130  facwordi  11161  hashunlem  11227  ssenneg  11263  zfz1isolemiso  11274  seq3coll  11277  swrdccat3blem  11494  caucvgrelemcau  11729  caucvgre  11730  cvg1nlemcau  11733  cvg1nlemres  11734  recvguniq  11744  resqrexlemover  11759  resqrexlemgt0  11769  resqrexlemoverl  11770  resqrexlemglsq  11771  resqrexlemsqa  11773  resqrexlemex  11774  maxleastlt  11964  minmax  11979  lemininf  11983  ltmininf  11984  xrmaxleastlt  12005  xrmaxltsup  12007  xrminmax  12014  xrmin1inf  12016  xrmin2inf  12017  xrltmininf  12019  xrlemininf  12020  climserle  12094  summodclem3  12130  summodclem2a  12131  summodc  12133  zsumdc  12134  fsum3  12137  fsum00  12212  fsumabs  12215  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  zproddc  12329  fprodseq  12333  fprodle  12390  sin01bnd  12507  cos01bnd  12508  summodnegmod  12572  modmulconst  12573  dvdsaddr  12587  dvdssub  12588  dvdssubr  12589  dvdslelemd  12593  dvdsfac  12610  dvdsmod  12612  oddp1even  12626  ltoddhalfle  12643  opoe  12645  omoe  12646  divalg2  12676  divalgmod  12677  ndvdssub  12680  ndvdsadd  12681  bitsfval  12692  bitsval  12693  bits0  12698  bitsp1  12701  bitsfzolem  12704  bitsfzo  12705  bitscmp  12708  bitsinv1lem  12711  bezoutlembi  12765  dvdssqim  12784  dvdsmulgcd  12785  dvdssq  12791  nn0seqcvgd  12802  coprmdvds  12853  coprmdvds2  12854  rpmul  12859  cncongr1  12864  divgcdodd  12904  isprm6  12908  prmdvdsexp  12909  prmdvdsexpr  12911  prmfac1  12913  oddpwdclemxy  12930  oddpwdclemodd  12933  sqpweven  12936  2sqpwodd  12937  sqne2sq  12938  hashdvds  12982  phiprmpw  12983  eulerthlemh  12992  prmdiv  12996  prmdiveq  12997  odzval  13003  odzcllem  13004  odzdvds  13007  pythagtriplem11  13036  pythagtriplem13  13038  pythagtrip  13045  pceulem  13056  pczndvds2  13080  pcdvdsb  13082  pc2dvds  13092  pcz  13094  pcprmpw2  13095  dvdsprmpweq  13097  dvdsprmpweqle  13099  difsqpwdvds  13100  pcmpt  13105  prmpwdvds  13117  pockthlem  13118  4sqlem11  13163  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfileme  13219  ballotfilemefi  13220  ballotfilemodife  13223  ballotfilem4  13224  ballotfilem1c  13234  ballotfilemsval  13235  ballotfilemieq  13243  ballotfilemfrcn0  13256  ballotfi  13265  exmidunben  13300  nninfdclemlt  13325  mulgval  13908  dvdsrtr  14391  dvdsrmul1  14392  unitnegcl  14420  unitpropdg  14438  elrhmunit  14467  zndvds0  14968  znunit  14977  mplsubgfilemcl  15073  psmettri2  15412  ismet2  15438  xmettri2  15445  comet  15583  ivthinclemum  15719  ivthinclemlopn  15720  ivthinclemlr  15721  ivthinclemuopn  15722  ivthinclemur  15723  ivthinclemdisj  15724  ivthinclemloc  15725  ivthinc  15727  ivthreinc  15729  limccl  15743  ellimc3apf  15744  sin0pilem2  15866  pilem3  15867  sincosq1sgn  15910  sincosq2sgn  15911  sincosq4sgn  15913  logltb  15958  logle1b  15976  loglt1b  15977  logbgt0b  16051  wilthlem1  16077  sgmval  16080  dvdsppwf1o  16086  perfect1  16095  lgslem1  16102  lgsval  16106  lgsdilem  16129  lgsne0  16140  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  lgseisenlem1  16172  lgseisenlem2  16173  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad2lem2  16184  m1lgs  16187  2lgslem1a1  16188  2lgslem1a  16190  2lgsoddprmlem2  16208  2lgsoddprmlem3  16213  2sqlem4  16220  2sqlem8a  16224  eupth2lem3lem3fi  16694  eupth2lem3lem6fi  16695  eupth2lem3lem4fi  16697  eupth2lem3lem7fi  16698  eupth2lemsfi  16702  eupth2fi  16703  konigsberglem4  16715