Theorem breq2d 4100

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 4092	. 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 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  breqtrd  4114  sbcbr1g  4145  pofun  4409  csbfv12g  5679  isorel  5949  isocnv  5952  isotr  5957  caovordig  6188  caovordg  6190  caovord  6194  xporderlem  6396  th3qlem2  6807  phplem3g  7042  supsnti  7204  inflbti  7223  difinfinf  7300  enqdc1  7582  ltanqg  7620  ltmnqg  7621  archnqq  7637  prarloclemarch2  7639  prloc  7711  addnqprllem  7747  addlocprlemgt  7754  appdivnq  7783  mulnqprl  7788  1idprl  7810  ltexprlemloc  7827  caucvgprlemcanl  7864  cauappcvgprlemm  7865  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  cauappcvgpr  7882  archrecnq  7883  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemcl  7896  caucvgprlemladdrl  7898  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgprpr  7932  ltposr  7983  ltasrg  7990  mulgt0sr  7998  mulextsr1lem  8000  mulextsr1  8001  prsrlt  8007  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsrlembound  8014  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  caucvgsr  8022  map2psrprg  8025  pitonnlem2  8067  pitonn  8068  recidpipr  8076  axpre-ltadd  8106  axpre-mulgt0  8107  axpre-mulext  8108  axarch  8111  nntopi  8114  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  ltaddneg  8604  ltsubadd2  8613  lesubadd2  8615  ltaddsub  8616  leaddsub  8618  ltaddpos2  8633  posdif  8635  lesub1  8636  ltsub1  8638  ltnegcon1  8643  lenegcon1  8646  addge02  8653  leaddle0  8657  ltordlem  8662  possumd  8749  sublt0d  8750  apreap  8767  prodgt02  9033  prodge02  9035  ltmulgt12  9045  lemulge12  9047  ltdivmul  9056  ledivmul  9057  ltdivmul2  9058  lt2mul2div  9059  ledivmul2  9060  ltrec  9063  ltrec1  9068  ltdiv23  9072  lediv23  9073  nnge1  9166  halfpos  9375  lt2halves  9380  addltmul  9381  avglt2  9384  avgle2  9386  nnrecl  9400  zltlem1  9537  difgtsumgt  9549  nn0le2is012  9562  gtndiv  9575  qapne  9873  nnledivrp  10001  xltnegi  10070  xltadd1  10111  xsubge0  10116  xposdif  10117  xlesubadd  10118  xleaddadd  10122  divelunit  10237  eluzgtdifelfzo  10443  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemshrink  10509  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2zlemshrink  10514  rebtwn2z  10515  flqlelt  10537  flqbi  10551  2tnp1ge0ge0  10562  q2submod  10648  frec2uzltd  10666  frec2uzlt2d  10667  frec2uzf1od  10669  monoord  10748  ser3mono  10750  ser3ge0  10799  expnbnd  10926  nn0ltexp2  10972  facwordi  11003  hashunlem  11068  zfz1isolemiso  11104  seq3coll  11107  swrdccat3blem  11321  caucvgrelemcau  11542  caucvgre  11543  cvg1nlemcau  11546  cvg1nlemres  11547  recvguniq  11557  resqrexlemover  11572  resqrexlemgt0  11582  resqrexlemoverl  11583  resqrexlemglsq  11584  resqrexlemsqa  11586  resqrexlemex  11587  maxleastlt  11777  minmax  11792  lemininf  11796  ltmininf  11797  xrmaxleastlt  11818  xrmaxltsup  11820  xrminmax  11827  xrmin1inf  11829  xrmin2inf  11830  xrltmininf  11832  xrlemininf  11833  climserle  11907  summodclem3  11943  summodclem2a  11944  summodc  11946  zsumdc  11947  fsum3  11950  fsum00  12025  fsumabs  12028  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  zproddc  12142  fprodseq  12146  fprodle  12203  sin01bnd  12320  cos01bnd  12321  summodnegmod  12385  modmulconst  12386  dvdsaddr  12400  dvdssub  12401  dvdssubr  12402  dvdslelemd  12406  dvdsfac  12423  dvdsmod  12425  oddp1even  12439  ltoddhalfle  12456  opoe  12458  omoe  12459  divalg2  12489  divalgmod  12490  ndvdssub  12493  ndvdsadd  12494  bitsfval  12505  bitsval  12506  bits0  12511  bitsp1  12514  bitsfzolem  12517  bitsfzo  12518  bitscmp  12521  bitsinv1lem  12524  bezoutlembi  12578  dvdssqim  12597  dvdsmulgcd  12598  dvdssq  12604  nn0seqcvgd  12615  coprmdvds  12666  coprmdvds2  12667  rpmul  12672  cncongr1  12677  divgcdodd  12717  isprm6  12721  prmdvdsexp  12722  prmdvdsexpr  12724  prmfac1  12726  oddpwdclemxy  12743  oddpwdclemodd  12746  sqpweven  12749  2sqpwodd  12750  sqne2sq  12751  hashdvds  12795  phiprmpw  12796  eulerthlemh  12805  prmdiv  12809  prmdiveq  12810  odzval  12816  odzcllem  12817  odzdvds  12820  pythagtriplem11  12849  pythagtriplem13  12851  pythagtrip  12858  pceulem  12869  pczndvds2  12893  pcdvdsb  12895  pc2dvds  12905  pcz  12907  pcprmpw2  12908  dvdsprmpweq  12910  dvdsprmpweqle  12912  difsqpwdvds  12913  pcmpt  12918  prmpwdvds  12930  pockthlem  12931  4sqlem11  12976  exmidunben  13049  nninfdclemlt  13074  mulgval  13711  dvdsrtr  14118  dvdsrmul1  14119  unitnegcl  14147  unitpropdg  14165  elrhmunit  14194  zndvds0  14667  znunit  14676  mplsubgfilemcl  14716  psmettri2  15055  ismet2  15081  xmettri2  15088  comet  15226  ivthinclemum  15362  ivthinclemlopn  15363  ivthinclemlr  15364  ivthinclemuopn  15365  ivthinclemur  15366  ivthinclemdisj  15367  ivthinclemloc  15368  ivthinc  15370  ivthreinc  15372  limccl  15386  ellimc3apf  15387  sin0pilem2  15509  pilem3  15510  sincosq1sgn  15553  sincosq2sgn  15554  sincosq4sgn  15556  logltb  15601  logle1b  15619  loglt1b  15620  logbgt0b  15693  wilthlem1  15707  sgmval  15710  dvdsppwf1o  15716  perfect1  15725  lgslem1  15732  lgsval  15736  lgsdilem  15759  lgsne0  15770  gausslemma2dlem1a  15790  gausslemma2dlem1f1o  15792  lgseisenlem1  15802  lgseisenlem2  15803  lgsquadlem1  15809  lgsquadlem2  15810  lgsquadlem3  15811  lgsquad2lem2  15814  m1lgs  15817  2lgslem1a1  15818  2lgslem1a  15820  2lgsoddprmlem2  15838  2lgsoddprmlem3  15843  2sqlem4  15850  2sqlem8a  15854  eupth2lem3lem3fi  16324  eupth2lem3lem6fi  16325  eupth2lem3lem4fi  16327  eupth2lem3lem7fi  16328  eupth2lemsfi  16332  eupth2fi  16333