Theorem breq2d 4074

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 4066	. 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 1375   class class class wbr 4062

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-v 2781  df-un 3181  df-sn 3652  df-pr 3653  df-op 3655  df-br 4063

This theorem is referenced by:  breqtrd  4088  sbcbr1g  4119  pofun  4380  csbfv12g  5641  isorel  5905  isocnv  5908  isotr  5913  caovordig  6142  caovordg  6144  caovord  6148  xporderlem  6347  th3qlem2  6755  phplem3g  6985  supsnti  7140  inflbti  7159  difinfinf  7236  enqdc1  7517  ltanqg  7555  ltmnqg  7556  archnqq  7572  prarloclemarch2  7574  prloc  7646  addnqprllem  7682  addlocprlemgt  7689  appdivnq  7718  mulnqprl  7723  1idprl  7745  ltexprlemloc  7762  caucvgprlemcanl  7799  cauappcvgprlemm  7800  cauappcvgprlemladdru  7811  cauappcvgprlemladdrl  7812  cauappcvgprlem1  7814  cauappcvgprlemlim  7816  cauappcvgpr  7817  archrecnq  7818  caucvgprlemnkj  7821  caucvgprlemnbj  7822  caucvgprlemm  7823  caucvgprlemcl  7831  caucvgprlemladdrl  7833  caucvgpr  7837  caucvgprprlemell  7840  caucvgprprlemelu  7841  caucvgprprlemcbv  7842  caucvgprprlemval  7843  caucvgprprlemnkeqj  7845  caucvgprprlemml  7849  caucvgprprlemmu  7850  caucvgprprlemopl  7852  caucvgprprlemlol  7853  caucvgprprlemopu  7854  caucvgprprlemloc  7858  caucvgprprlemclphr  7860  caucvgprprlemexbt  7861  caucvgprprlem1  7864  caucvgprprlem2  7865  caucvgprpr  7867  ltposr  7918  ltasrg  7925  mulgt0sr  7933  mulextsr1lem  7935  mulextsr1  7936  prsrlt  7942  caucvgsrlemcl  7944  caucvgsrlemfv  7946  caucvgsrlembound  7949  caucvgsrlemgt1  7950  caucvgsrlemoffres  7955  caucvgsr  7957  map2psrprg  7960  pitonnlem2  8002  pitonn  8003  recidpipr  8011  axpre-ltadd  8041  axpre-mulgt0  8042  axpre-mulext  8043  axarch  8046  nntopi  8049  axcaucvglemval  8052  axcaucvglemcau  8053  axcaucvglemres  8054  axpre-suploclemres  8056  ltaddneg  8539  ltsubadd2  8548  lesubadd2  8550  ltaddsub  8551  leaddsub  8553  ltaddpos2  8568  posdif  8570  lesub1  8571  ltsub1  8573  ltnegcon1  8578  lenegcon1  8581  addge02  8588  leaddle0  8592  ltordlem  8597  possumd  8684  sublt0d  8685  apreap  8702  prodgt02  8968  prodge02  8970  ltmulgt12  8980  lemulge12  8982  ltdivmul  8991  ledivmul  8992  ltdivmul2  8993  lt2mul2div  8994  ledivmul2  8995  ltrec  8998  ltrec1  9003  ltdiv23  9007  lediv23  9008  nnge1  9101  halfpos  9310  lt2halves  9315  addltmul  9316  avglt2  9319  avgle2  9321  nnrecl  9335  zltlem1  9472  difgtsumgt  9484  nn0le2is012  9497  gtndiv  9510  qapne  9802  nnledivrp  9930  xltnegi  9999  xltadd1  10040  xsubge0  10045  xposdif  10046  xlesubadd  10047  xleaddadd  10051  divelunit  10166  eluzgtdifelfzo  10370  qtri3or  10427  exbtwnzlemstep  10434  exbtwnzlemshrink  10435  exbtwnzlemex  10436  exbtwnz  10437  rebtwn2zlemstep  10439  rebtwn2zlemshrink  10440  rebtwn2z  10441  flqlelt  10463  flqbi  10477  2tnp1ge0ge0  10488  q2submod  10574  frec2uzltd  10592  frec2uzlt2d  10593  frec2uzf1od  10595  monoord  10674  ser3mono  10676  ser3ge0  10725  expnbnd  10852  nn0ltexp2  10898  facwordi  10929  hashunlem  10993  zfz1isolemiso  11028  seq3coll  11031  swrdccat3blem  11237  caucvgrelemcau  11457  caucvgre  11458  cvg1nlemcau  11461  cvg1nlemres  11462  recvguniq  11472  resqrexlemover  11487  resqrexlemgt0  11497  resqrexlemoverl  11498  resqrexlemglsq  11499  resqrexlemsqa  11501  resqrexlemex  11502  maxleastlt  11692  minmax  11707  lemininf  11711  ltmininf  11712  xrmaxleastlt  11733  xrmaxltsup  11735  xrminmax  11742  xrmin1inf  11744  xrmin2inf  11745  xrltmininf  11747  xrlemininf  11748  climserle  11822  summodclem3  11857  summodclem2a  11858  summodc  11860  zsumdc  11861  fsum3  11864  fsum00  11939  fsumabs  11942  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  zproddc  12056  fprodseq  12060  fprodle  12117  sin01bnd  12234  cos01bnd  12235  summodnegmod  12299  modmulconst  12300  dvdsaddr  12314  dvdssub  12315  dvdssubr  12316  dvdslelemd  12320  dvdsfac  12337  dvdsmod  12339  oddp1even  12353  ltoddhalfle  12370  opoe  12372  omoe  12373  divalg2  12403  divalgmod  12404  ndvdssub  12407  ndvdsadd  12408  bitsfval  12419  bitsval  12420  bits0  12425  bitsp1  12428  bitsfzolem  12431  bitsfzo  12432  bitscmp  12435  bitsinv1lem  12438  bezoutlembi  12492  dvdssqim  12511  dvdsmulgcd  12512  dvdssq  12518  nn0seqcvgd  12529  coprmdvds  12580  coprmdvds2  12581  rpmul  12586  cncongr1  12591  divgcdodd  12631  isprm6  12635  prmdvdsexp  12636  prmdvdsexpr  12638  prmfac1  12640  oddpwdclemxy  12657  oddpwdclemodd  12660  sqpweven  12663  2sqpwodd  12664  sqne2sq  12665  hashdvds  12709  phiprmpw  12710  eulerthlemh  12719  prmdiv  12723  prmdiveq  12724  odzval  12730  odzcllem  12731  odzdvds  12734  pythagtriplem11  12763  pythagtriplem13  12765  pythagtrip  12772  pceulem  12783  pczndvds2  12807  pcdvdsb  12809  pc2dvds  12819  pcz  12821  pcprmpw2  12822  dvdsprmpweq  12824  dvdsprmpweqle  12826  difsqpwdvds  12827  pcmpt  12832  prmpwdvds  12844  pockthlem  12845  4sqlem11  12890  exmidunben  12963  nninfdclemlt  12988  mulgval  13625  dvdsrtr  14030  dvdsrmul1  14031  unitnegcl  14059  unitpropdg  14077  elrhmunit  14106  zndvds0  14579  znunit  14588  mplsubgfilemcl  14628  psmettri2  14967  ismet2  14993  xmettri2  15000  comet  15138  ivthinclemum  15274  ivthinclemlopn  15275  ivthinclemlr  15276  ivthinclemuopn  15277  ivthinclemur  15278  ivthinclemdisj  15279  ivthinclemloc  15280  ivthinc  15282  ivthreinc  15284  limccl  15298  ellimc3apf  15299  sin0pilem2  15421  pilem3  15422  sincosq1sgn  15465  sincosq2sgn  15466  sincosq4sgn  15468  logltb  15513  logle1b  15531  loglt1b  15532  logbgt0b  15605  wilthlem1  15619  sgmval  15622  dvdsppwf1o  15628  perfect1  15637  lgslem1  15644  lgsval  15648  lgsdilem  15671  lgsne0  15682  gausslemma2dlem1a  15702  gausslemma2dlem1f1o  15704  lgseisenlem1  15714  lgseisenlem2  15715  lgsquadlem1  15721  lgsquadlem2  15722  lgsquadlem3  15723  lgsquad2lem2  15726  m1lgs  15729  2lgslem1a1  15730  2lgslem1a  15732  2lgsoddprmlem2  15750  2lgsoddprmlem3  15755  2sqlem4  15762  2sqlem8a  15766