Theorem breq2d 4098

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 4090	. 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 4086

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  breqtrd  4112  sbcbr1g  4143  pofun  4407  csbfv12g  5675  isorel  5944  isocnv  5947  isotr  5952  caovordig  6183  caovordg  6185  caovord  6189  xporderlem  6391  th3qlem2  6802  phplem3g  7037  supsnti  7198  inflbti  7217  difinfinf  7294  enqdc1  7575  ltanqg  7613  ltmnqg  7614  archnqq  7630  prarloclemarch2  7632  prloc  7704  addnqprllem  7740  addlocprlemgt  7747  appdivnq  7776  mulnqprl  7781  1idprl  7803  ltexprlemloc  7820  caucvgprlemcanl  7857  cauappcvgprlemm  7858  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  cauappcvgprlem1  7872  cauappcvgprlemlim  7874  cauappcvgpr  7875  archrecnq  7876  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprlemm  7881  caucvgprlemcl  7889  caucvgprlemladdrl  7891  caucvgpr  7895  caucvgprprlemell  7898  caucvgprprlemelu  7899  caucvgprprlemcbv  7900  caucvgprprlemval  7901  caucvgprprlemnkeqj  7903  caucvgprprlemml  7907  caucvgprprlemmu  7908  caucvgprprlemopl  7910  caucvgprprlemlol  7911  caucvgprprlemopu  7912  caucvgprprlemloc  7916  caucvgprprlemclphr  7918  caucvgprprlemexbt  7919  caucvgprprlem1  7922  caucvgprprlem2  7923  caucvgprpr  7925  ltposr  7976  ltasrg  7983  mulgt0sr  7991  mulextsr1lem  7993  mulextsr1  7994  prsrlt  8000  caucvgsrlemcl  8002  caucvgsrlemfv  8004  caucvgsrlembound  8007  caucvgsrlemgt1  8008  caucvgsrlemoffres  8013  caucvgsr  8015  map2psrprg  8018  pitonnlem2  8060  pitonn  8061  recidpipr  8069  axpre-ltadd  8099  axpre-mulgt0  8100  axpre-mulext  8101  axarch  8104  nntopi  8107  axcaucvglemval  8110  axcaucvglemcau  8111  axcaucvglemres  8112  axpre-suploclemres  8114  ltaddneg  8597  ltsubadd2  8606  lesubadd2  8608  ltaddsub  8609  leaddsub  8611  ltaddpos2  8626  posdif  8628  lesub1  8629  ltsub1  8631  ltnegcon1  8636  lenegcon1  8639  addge02  8646  leaddle0  8650  ltordlem  8655  possumd  8742  sublt0d  8743  apreap  8760  prodgt02  9026  prodge02  9028  ltmulgt12  9038  lemulge12  9040  ltdivmul  9049  ledivmul  9050  ltdivmul2  9051  lt2mul2div  9052  ledivmul2  9053  ltrec  9056  ltrec1  9061  ltdiv23  9065  lediv23  9066  nnge1  9159  halfpos  9368  lt2halves  9373  addltmul  9374  avglt2  9377  avgle2  9379  nnrecl  9393  zltlem1  9530  difgtsumgt  9542  nn0le2is012  9555  gtndiv  9568  qapne  9866  nnledivrp  9994  xltnegi  10063  xltadd1  10104  xsubge0  10109  xposdif  10110  xlesubadd  10111  xleaddadd  10115  divelunit  10230  eluzgtdifelfzo  10435  qtri3or  10493  exbtwnzlemstep  10500  exbtwnzlemshrink  10501  exbtwnzlemex  10502  exbtwnz  10503  rebtwn2zlemstep  10505  rebtwn2zlemshrink  10506  rebtwn2z  10507  flqlelt  10529  flqbi  10543  2tnp1ge0ge0  10554  q2submod  10640  frec2uzltd  10658  frec2uzlt2d  10659  frec2uzf1od  10661  monoord  10740  ser3mono  10742  ser3ge0  10791  expnbnd  10918  nn0ltexp2  10964  facwordi  10995  hashunlem  11060  zfz1isolemiso  11096  seq3coll  11099  swrdccat3blem  11313  caucvgrelemcau  11534  caucvgre  11535  cvg1nlemcau  11538  cvg1nlemres  11539  recvguniq  11549  resqrexlemover  11564  resqrexlemgt0  11574  resqrexlemoverl  11575  resqrexlemglsq  11576  resqrexlemsqa  11578  resqrexlemex  11579  maxleastlt  11769  minmax  11784  lemininf  11788  ltmininf  11789  xrmaxleastlt  11810  xrmaxltsup  11812  xrminmax  11819  xrmin1inf  11821  xrmin2inf  11822  xrltmininf  11824  xrlemininf  11825  climserle  11899  summodclem3  11934  summodclem2a  11935  summodc  11937  zsumdc  11938  fsum3  11941  fsum00  12016  fsumabs  12019  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  zproddc  12133  fprodseq  12137  fprodle  12194  sin01bnd  12311  cos01bnd  12312  summodnegmod  12376  modmulconst  12377  dvdsaddr  12391  dvdssub  12392  dvdssubr  12393  dvdslelemd  12397  dvdsfac  12414  dvdsmod  12416  oddp1even  12430  ltoddhalfle  12447  opoe  12449  omoe  12450  divalg2  12480  divalgmod  12481  ndvdssub  12484  ndvdsadd  12485  bitsfval  12496  bitsval  12497  bits0  12502  bitsp1  12505  bitsfzolem  12508  bitsfzo  12509  bitscmp  12512  bitsinv1lem  12515  bezoutlembi  12569  dvdssqim  12588  dvdsmulgcd  12589  dvdssq  12595  nn0seqcvgd  12606  coprmdvds  12657  coprmdvds2  12658  rpmul  12663  cncongr1  12668  divgcdodd  12708  isprm6  12712  prmdvdsexp  12713  prmdvdsexpr  12715  prmfac1  12717  oddpwdclemxy  12734  oddpwdclemodd  12737  sqpweven  12740  2sqpwodd  12741  sqne2sq  12742  hashdvds  12786  phiprmpw  12787  eulerthlemh  12796  prmdiv  12800  prmdiveq  12801  odzval  12807  odzcllem  12808  odzdvds  12811  pythagtriplem11  12840  pythagtriplem13  12842  pythagtrip  12849  pceulem  12860  pczndvds2  12884  pcdvdsb  12886  pc2dvds  12896  pcz  12898  pcprmpw2  12899  dvdsprmpweq  12901  dvdsprmpweqle  12903  difsqpwdvds  12904  pcmpt  12909  prmpwdvds  12921  pockthlem  12922  4sqlem11  12967  exmidunben  13040  nninfdclemlt  13065  mulgval  13702  dvdsrtr  14108  dvdsrmul1  14109  unitnegcl  14137  unitpropdg  14155  elrhmunit  14184  zndvds0  14657  znunit  14666  mplsubgfilemcl  14706  psmettri2  15045  ismet2  15071  xmettri2  15078  comet  15216  ivthinclemum  15352  ivthinclemlopn  15353  ivthinclemlr  15354  ivthinclemuopn  15355  ivthinclemur  15356  ivthinclemdisj  15357  ivthinclemloc  15358  ivthinc  15360  ivthreinc  15362  limccl  15376  ellimc3apf  15377  sin0pilem2  15499  pilem3  15500  sincosq1sgn  15543  sincosq2sgn  15544  sincosq4sgn  15546  logltb  15591  logle1b  15609  loglt1b  15610  logbgt0b  15683  wilthlem1  15697  sgmval  15700  dvdsppwf1o  15706  perfect1  15715  lgslem1  15722  lgsval  15726  lgsdilem  15749  lgsne0  15760  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  lgseisenlem1  15792  lgseisenlem2  15793  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad2lem2  15804  m1lgs  15807  2lgslem1a1  15808  2lgslem1a  15810  2lgsoddprmlem2  15828  2lgsoddprmlem3  15833  2sqlem4  15840  2sqlem8a  15844