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  4403  csbfv12g  5669  isorel  5938  isocnv  5941  isotr  5946  caovordig  6177  caovordg  6179  caovord  6183  xporderlem  6383  th3qlem2  6793  phplem3g  7025  supsnti  7180  inflbti  7199  difinfinf  7276  enqdc1  7557  ltanqg  7595  ltmnqg  7596  archnqq  7612  prarloclemarch2  7614  prloc  7686  addnqprllem  7722  addlocprlemgt  7729  appdivnq  7758  mulnqprl  7763  1idprl  7785  ltexprlemloc  7802  caucvgprlemcanl  7839  cauappcvgprlemm  7840  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  cauappcvgprlem1  7854  cauappcvgprlemlim  7856  cauappcvgpr  7857  archrecnq  7858  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemm  7863  caucvgprlemcl  7871  caucvgprlemladdrl  7873  caucvgpr  7877  caucvgprprlemell  7880  caucvgprprlemelu  7881  caucvgprprlemcbv  7882  caucvgprprlemval  7883  caucvgprprlemnkeqj  7885  caucvgprprlemml  7889  caucvgprprlemmu  7890  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemopu  7894  caucvgprprlemloc  7898  caucvgprprlemclphr  7900  caucvgprprlemexbt  7901  caucvgprprlem1  7904  caucvgprprlem2  7905  caucvgprpr  7907  ltposr  7958  ltasrg  7965  mulgt0sr  7973  mulextsr1lem  7975  mulextsr1  7976  prsrlt  7982  caucvgsrlemcl  7984  caucvgsrlemfv  7986  caucvgsrlembound  7989  caucvgsrlemgt1  7990  caucvgsrlemoffres  7995  caucvgsr  7997  map2psrprg  8000  pitonnlem2  8042  pitonn  8043  recidpipr  8051  axpre-ltadd  8081  axpre-mulgt0  8082  axpre-mulext  8083  axarch  8086  nntopi  8089  axcaucvglemval  8092  axcaucvglemcau  8093  axcaucvglemres  8094  axpre-suploclemres  8096  ltaddneg  8579  ltsubadd2  8588  lesubadd2  8590  ltaddsub  8591  leaddsub  8593  ltaddpos2  8608  posdif  8610  lesub1  8611  ltsub1  8613  ltnegcon1  8618  lenegcon1  8621  addge02  8628  leaddle0  8632  ltordlem  8637  possumd  8724  sublt0d  8725  apreap  8742  prodgt02  9008  prodge02  9010  ltmulgt12  9020  lemulge12  9022  ltdivmul  9031  ledivmul  9032  ltdivmul2  9033  lt2mul2div  9034  ledivmul2  9035  ltrec  9038  ltrec1  9043  ltdiv23  9047  lediv23  9048  nnge1  9141  halfpos  9350  lt2halves  9355  addltmul  9356  avglt2  9359  avgle2  9361  nnrecl  9375  zltlem1  9512  difgtsumgt  9524  nn0le2is012  9537  gtndiv  9550  qapne  9842  nnledivrp  9970  xltnegi  10039  xltadd1  10080  xsubge0  10085  xposdif  10086  xlesubadd  10087  xleaddadd  10091  divelunit  10206  eluzgtdifelfzo  10411  qtri3or  10468  exbtwnzlemstep  10475  exbtwnzlemshrink  10476  exbtwnzlemex  10477  exbtwnz  10478  rebtwn2zlemstep  10480  rebtwn2zlemshrink  10481  rebtwn2z  10482  flqlelt  10504  flqbi  10518  2tnp1ge0ge0  10529  q2submod  10615  frec2uzltd  10633  frec2uzlt2d  10634  frec2uzf1od  10636  monoord  10715  ser3mono  10717  ser3ge0  10766  expnbnd  10893  nn0ltexp2  10939  facwordi  10970  hashunlem  11034  zfz1isolemiso  11069  seq3coll  11072  swrdccat3blem  11279  caucvgrelemcau  11499  caucvgre  11500  cvg1nlemcau  11503  cvg1nlemres  11504  recvguniq  11514  resqrexlemover  11529  resqrexlemgt0  11539  resqrexlemoverl  11540  resqrexlemglsq  11541  resqrexlemsqa  11543  resqrexlemex  11544  maxleastlt  11734  minmax  11749  lemininf  11753  ltmininf  11754  xrmaxleastlt  11775  xrmaxltsup  11777  xrminmax  11784  xrmin1inf  11786  xrmin2inf  11787  xrltmininf  11789  xrlemininf  11790  climserle  11864  summodclem3  11899  summodclem2a  11900  summodc  11902  zsumdc  11903  fsum3  11906  fsum00  11981  fsumabs  11984  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  zproddc  12098  fprodseq  12102  fprodle  12159  sin01bnd  12276  cos01bnd  12277  summodnegmod  12341  modmulconst  12342  dvdsaddr  12356  dvdssub  12357  dvdssubr  12358  dvdslelemd  12362  dvdsfac  12379  dvdsmod  12381  oddp1even  12395  ltoddhalfle  12412  opoe  12414  omoe  12415  divalg2  12445  divalgmod  12446  ndvdssub  12449  ndvdsadd  12450  bitsfval  12461  bitsval  12462  bits0  12467  bitsp1  12470  bitsfzolem  12473  bitsfzo  12474  bitscmp  12477  bitsinv1lem  12480  bezoutlembi  12534  dvdssqim  12553  dvdsmulgcd  12554  dvdssq  12560  nn0seqcvgd  12571  coprmdvds  12622  coprmdvds2  12623  rpmul  12628  cncongr1  12633  divgcdodd  12673  isprm6  12677  prmdvdsexp  12678  prmdvdsexpr  12680  prmfac1  12682  oddpwdclemxy  12699  oddpwdclemodd  12702  sqpweven  12705  2sqpwodd  12706  sqne2sq  12707  hashdvds  12751  phiprmpw  12752  eulerthlemh  12761  prmdiv  12765  prmdiveq  12766  odzval  12772  odzcllem  12773  odzdvds  12776  pythagtriplem11  12805  pythagtriplem13  12807  pythagtrip  12814  pceulem  12825  pczndvds2  12849  pcdvdsb  12851  pc2dvds  12861  pcz  12863  pcprmpw2  12864  dvdsprmpweq  12866  dvdsprmpweqle  12868  difsqpwdvds  12869  pcmpt  12874  prmpwdvds  12886  pockthlem  12887  4sqlem11  12932  exmidunben  13005  nninfdclemlt  13030  mulgval  13667  dvdsrtr  14073  dvdsrmul1  14074  unitnegcl  14102  unitpropdg  14120  elrhmunit  14149  zndvds0  14622  znunit  14631  mplsubgfilemcl  14671  psmettri2  15010  ismet2  15036  xmettri2  15043  comet  15181  ivthinclemum  15317  ivthinclemlopn  15318  ivthinclemlr  15319  ivthinclemuopn  15320  ivthinclemur  15321  ivthinclemdisj  15322  ivthinclemloc  15323  ivthinc  15325  ivthreinc  15327  limccl  15341  ellimc3apf  15342  sin0pilem2  15464  pilem3  15465  sincosq1sgn  15508  sincosq2sgn  15509  sincosq4sgn  15511  logltb  15556  logle1b  15574  loglt1b  15575  logbgt0b  15648  wilthlem1  15662  sgmval  15665  dvdsppwf1o  15671  perfect1  15680  lgslem1  15687  lgsval  15691  lgsdilem  15714  lgsne0  15725  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  lgseisenlem1  15757  lgseisenlem2  15758  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2lem2  15769  m1lgs  15772  2lgslem1a1  15773  2lgslem1a  15775  2lgsoddprmlem2  15793  2lgsoddprmlem3  15798  2sqlem4  15805  2sqlem8a  15809