Theorem breq2d 4095

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 4087	. 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 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breqtrd  4109  sbcbr1g  4140  pofun  4404  csbfv12g  5672  isorel  5941  isocnv  5944  isotr  5949  caovordig  6180  caovordg  6182  caovord  6186  xporderlem  6388  th3qlem2  6798  phplem3g  7030  supsnti  7188  inflbti  7207  difinfinf  7284  enqdc1  7565  ltanqg  7603  ltmnqg  7604  archnqq  7620  prarloclemarch2  7622  prloc  7694  addnqprllem  7730  addlocprlemgt  7737  appdivnq  7766  mulnqprl  7771  1idprl  7793  ltexprlemloc  7810  caucvgprlemcanl  7847  cauappcvgprlemm  7848  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  cauappcvgprlem1  7862  cauappcvgprlemlim  7864  cauappcvgpr  7865  archrecnq  7866  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemm  7871  caucvgprlemcl  7879  caucvgprlemladdrl  7881  caucvgpr  7885  caucvgprprlemell  7888  caucvgprprlemelu  7889  caucvgprprlemcbv  7890  caucvgprprlemval  7891  caucvgprprlemnkeqj  7893  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemopu  7902  caucvgprprlemloc  7906  caucvgprprlemclphr  7908  caucvgprprlemexbt  7909  caucvgprprlem1  7912  caucvgprprlem2  7913  caucvgprpr  7915  ltposr  7966  ltasrg  7973  mulgt0sr  7981  mulextsr1lem  7983  mulextsr1  7984  prsrlt  7990  caucvgsrlemcl  7992  caucvgsrlemfv  7994  caucvgsrlembound  7997  caucvgsrlemgt1  7998  caucvgsrlemoffres  8003  caucvgsr  8005  map2psrprg  8008  pitonnlem2  8050  pitonn  8051  recidpipr  8059  axpre-ltadd  8089  axpre-mulgt0  8090  axpre-mulext  8091  axarch  8094  nntopi  8097  axcaucvglemval  8100  axcaucvglemcau  8101  axcaucvglemres  8102  axpre-suploclemres  8104  ltaddneg  8587  ltsubadd2  8596  lesubadd2  8598  ltaddsub  8599  leaddsub  8601  ltaddpos2  8616  posdif  8618  lesub1  8619  ltsub1  8621  ltnegcon1  8626  lenegcon1  8629  addge02  8636  leaddle0  8640  ltordlem  8645  possumd  8732  sublt0d  8733  apreap  8750  prodgt02  9016  prodge02  9018  ltmulgt12  9028  lemulge12  9030  ltdivmul  9039  ledivmul  9040  ltdivmul2  9041  lt2mul2div  9042  ledivmul2  9043  ltrec  9046  ltrec1  9051  ltdiv23  9055  lediv23  9056  nnge1  9149  halfpos  9358  lt2halves  9363  addltmul  9364  avglt2  9367  avgle2  9369  nnrecl  9383  zltlem1  9520  difgtsumgt  9532  nn0le2is012  9545  gtndiv  9558  qapne  9851  nnledivrp  9979  xltnegi  10048  xltadd1  10089  xsubge0  10094  xposdif  10095  xlesubadd  10096  xleaddadd  10100  divelunit  10215  eluzgtdifelfzo  10420  qtri3or  10477  exbtwnzlemstep  10484  exbtwnzlemshrink  10485  exbtwnzlemex  10486  exbtwnz  10487  rebtwn2zlemstep  10489  rebtwn2zlemshrink  10490  rebtwn2z  10491  flqlelt  10513  flqbi  10527  2tnp1ge0ge0  10538  q2submod  10624  frec2uzltd  10642  frec2uzlt2d  10643  frec2uzf1od  10645  monoord  10724  ser3mono  10726  ser3ge0  10775  expnbnd  10902  nn0ltexp2  10948  facwordi  10979  hashunlem  11043  zfz1isolemiso  11079  seq3coll  11082  swrdccat3blem  11292  caucvgrelemcau  11512  caucvgre  11513  cvg1nlemcau  11516  cvg1nlemres  11517  recvguniq  11527  resqrexlemover  11542  resqrexlemgt0  11552  resqrexlemoverl  11553  resqrexlemglsq  11554  resqrexlemsqa  11556  resqrexlemex  11557  maxleastlt  11747  minmax  11762  lemininf  11766  ltmininf  11767  xrmaxleastlt  11788  xrmaxltsup  11790  xrminmax  11797  xrmin1inf  11799  xrmin2inf  11800  xrltmininf  11802  xrlemininf  11803  climserle  11877  summodclem3  11912  summodclem2a  11913  summodc  11915  zsumdc  11916  fsum3  11919  fsum00  11994  fsumabs  11997  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  zproddc  12111  fprodseq  12115  fprodle  12172  sin01bnd  12289  cos01bnd  12290  summodnegmod  12354  modmulconst  12355  dvdsaddr  12369  dvdssub  12370  dvdssubr  12371  dvdslelemd  12375  dvdsfac  12392  dvdsmod  12394  oddp1even  12408  ltoddhalfle  12425  opoe  12427  omoe  12428  divalg2  12458  divalgmod  12459  ndvdssub  12462  ndvdsadd  12463  bitsfval  12474  bitsval  12475  bits0  12480  bitsp1  12483  bitsfzolem  12486  bitsfzo  12487  bitscmp  12490  bitsinv1lem  12493  bezoutlembi  12547  dvdssqim  12566  dvdsmulgcd  12567  dvdssq  12573  nn0seqcvgd  12584  coprmdvds  12635  coprmdvds2  12636  rpmul  12641  cncongr1  12646  divgcdodd  12686  isprm6  12690  prmdvdsexp  12691  prmdvdsexpr  12693  prmfac1  12695  oddpwdclemxy  12712  oddpwdclemodd  12715  sqpweven  12718  2sqpwodd  12719  sqne2sq  12720  hashdvds  12764  phiprmpw  12765  eulerthlemh  12774  prmdiv  12778  prmdiveq  12779  odzval  12785  odzcllem  12786  odzdvds  12789  pythagtriplem11  12818  pythagtriplem13  12820  pythagtrip  12827  pceulem  12838  pczndvds2  12862  pcdvdsb  12864  pc2dvds  12874  pcz  12876  pcprmpw2  12877  dvdsprmpweq  12879  dvdsprmpweqle  12881  difsqpwdvds  12882  pcmpt  12887  prmpwdvds  12899  pockthlem  12900  4sqlem11  12945  exmidunben  13018  nninfdclemlt  13043  mulgval  13680  dvdsrtr  14086  dvdsrmul1  14087  unitnegcl  14115  unitpropdg  14133  elrhmunit  14162  zndvds0  14635  znunit  14644  mplsubgfilemcl  14684  psmettri2  15023  ismet2  15049  xmettri2  15056  comet  15194  ivthinclemum  15330  ivthinclemlopn  15331  ivthinclemlr  15332  ivthinclemuopn  15333  ivthinclemur  15334  ivthinclemdisj  15335  ivthinclemloc  15336  ivthinc  15338  ivthreinc  15340  limccl  15354  ellimc3apf  15355  sin0pilem2  15477  pilem3  15478  sincosq1sgn  15521  sincosq2sgn  15522  sincosq4sgn  15524  logltb  15569  logle1b  15587  loglt1b  15588  logbgt0b  15661  wilthlem1  15675  sgmval  15678  dvdsppwf1o  15684  perfect1  15693  lgslem1  15700  lgsval  15704  lgsdilem  15727  lgsne0  15738  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  lgseisenlem1  15770  lgseisenlem2  15771  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad2lem2  15782  m1lgs  15785  2lgslem1a1  15786  2lgslem1a  15788  2lgsoddprmlem2  15806  2lgsoddprmlem3  15811  2sqlem4  15818  2sqlem8a  15822