Theorem breq2d 4101

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 4093	. 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 4089

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 2212

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203  df-sn 3676  df-pr 3677  df-op 3679  df-br 4090

This theorem is referenced by:  breqtrd  4115  sbcbr1g  4146  pofun  4411  csbfv12g  5682  isorel  5954  isocnv  5957  isotr  5962  caovordig  6193  caovordg  6195  caovord  6199  xporderlem  6401  th3qlem2  6812  phplem3g  7047  supsnti  7209  inflbti  7228  difinfinf  7305  enqdc1  7587  ltanqg  7625  ltmnqg  7626  archnqq  7642  prarloclemarch2  7644  prloc  7716  addnqprllem  7752  addlocprlemgt  7759  appdivnq  7788  mulnqprl  7793  1idprl  7815  ltexprlemloc  7832  caucvgprlemcanl  7869  cauappcvgprlemm  7870  cauappcvgprlemladdru  7881  cauappcvgprlemladdrl  7882  cauappcvgprlem1  7884  cauappcvgprlemlim  7886  cauappcvgpr  7887  archrecnq  7888  caucvgprlemnkj  7891  caucvgprlemnbj  7892  caucvgprlemm  7893  caucvgprlemcl  7901  caucvgprlemladdrl  7903  caucvgpr  7907  caucvgprprlemell  7910  caucvgprprlemelu  7911  caucvgprprlemcbv  7912  caucvgprprlemval  7913  caucvgprprlemnkeqj  7915  caucvgprprlemml  7919  caucvgprprlemmu  7920  caucvgprprlemopl  7922  caucvgprprlemlol  7923  caucvgprprlemopu  7924  caucvgprprlemloc  7928  caucvgprprlemclphr  7930  caucvgprprlemexbt  7931  caucvgprprlem1  7934  caucvgprprlem2  7935  caucvgprpr  7937  ltposr  7988  ltasrg  7995  mulgt0sr  8003  mulextsr1lem  8005  mulextsr1  8006  prsrlt  8012  caucvgsrlemcl  8014  caucvgsrlemfv  8016  caucvgsrlembound  8019  caucvgsrlemgt1  8020  caucvgsrlemoffres  8025  caucvgsr  8027  map2psrprg  8030  pitonnlem2  8072  pitonn  8073  recidpipr  8081  axpre-ltadd  8111  axpre-mulgt0  8112  axpre-mulext  8113  axarch  8116  nntopi  8119  axcaucvglemval  8122  axcaucvglemcau  8123  axcaucvglemres  8124  axpre-suploclemres  8126  ltaddneg  8609  ltsubadd2  8618  lesubadd2  8620  ltaddsub  8621  leaddsub  8623  ltaddpos2  8638  posdif  8640  lesub1  8641  ltsub1  8643  ltnegcon1  8648  lenegcon1  8651  addge02  8658  leaddle0  8662  ltordlem  8667  possumd  8754  sublt0d  8755  apreap  8772  prodgt02  9038  prodge02  9040  ltmulgt12  9050  lemulge12  9052  ltdivmul  9061  ledivmul  9062  ltdivmul2  9063  lt2mul2div  9064  ledivmul2  9065  ltrec  9068  ltrec1  9073  ltdiv23  9077  lediv23  9078  nnge1  9171  halfpos  9380  lt2halves  9385  addltmul  9386  avglt2  9389  avgle2  9391  nnrecl  9405  zltlem1  9542  difgtsumgt  9554  nn0le2is012  9567  gtndiv  9580  qapne  9878  nnledivrp  10006  xltnegi  10075  xltadd1  10116  xsubge0  10121  xposdif  10122  xlesubadd  10123  xleaddadd  10127  divelunit  10242  eluzgtdifelfzo  10448  qtri3or  10506  exbtwnzlemstep  10513  exbtwnzlemshrink  10514  exbtwnzlemex  10515  exbtwnz  10516  rebtwn2zlemstep  10518  rebtwn2zlemshrink  10519  rebtwn2z  10520  flqlelt  10542  flqbi  10556  2tnp1ge0ge0  10567  q2submod  10653  frec2uzltd  10671  frec2uzlt2d  10672  frec2uzf1od  10674  monoord  10753  ser3mono  10755  ser3ge0  10804  expnbnd  10931  nn0ltexp2  10977  facwordi  11008  hashunlem  11073  zfz1isolemiso  11109  seq3coll  11112  swrdccat3blem  11329  caucvgrelemcau  11563  caucvgre  11564  cvg1nlemcau  11567  cvg1nlemres  11568  recvguniq  11578  resqrexlemover  11593  resqrexlemgt0  11603  resqrexlemoverl  11604  resqrexlemglsq  11605  resqrexlemsqa  11607  resqrexlemex  11608  maxleastlt  11798  minmax  11813  lemininf  11817  ltmininf  11818  xrmaxleastlt  11839  xrmaxltsup  11841  xrminmax  11848  xrmin1inf  11850  xrmin2inf  11851  xrltmininf  11853  xrlemininf  11854  climserle  11928  summodclem3  11964  summodclem2a  11965  summodc  11967  zsumdc  11968  fsum3  11971  fsum00  12046  fsumabs  12049  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  zproddc  12163  fprodseq  12167  fprodle  12224  sin01bnd  12341  cos01bnd  12342  summodnegmod  12406  modmulconst  12407  dvdsaddr  12421  dvdssub  12422  dvdssubr  12423  dvdslelemd  12427  dvdsfac  12444  dvdsmod  12446  oddp1even  12460  ltoddhalfle  12477  opoe  12479  omoe  12480  divalg2  12510  divalgmod  12511  ndvdssub  12514  ndvdsadd  12515  bitsfval  12526  bitsval  12527  bits0  12532  bitsp1  12535  bitsfzolem  12538  bitsfzo  12539  bitscmp  12542  bitsinv1lem  12545  bezoutlembi  12599  dvdssqim  12618  dvdsmulgcd  12619  dvdssq  12625  nn0seqcvgd  12636  coprmdvds  12687  coprmdvds2  12688  rpmul  12693  cncongr1  12698  divgcdodd  12738  isprm6  12742  prmdvdsexp  12743  prmdvdsexpr  12745  prmfac1  12747  oddpwdclemxy  12764  oddpwdclemodd  12767  sqpweven  12770  2sqpwodd  12771  sqne2sq  12772  hashdvds  12816  phiprmpw  12817  eulerthlemh  12826  prmdiv  12830  prmdiveq  12831  odzval  12837  odzcllem  12838  odzdvds  12841  pythagtriplem11  12870  pythagtriplem13  12872  pythagtrip  12879  pceulem  12890  pczndvds2  12914  pcdvdsb  12916  pc2dvds  12926  pcz  12928  pcprmpw2  12929  dvdsprmpweq  12931  dvdsprmpweqle  12933  difsqpwdvds  12934  pcmpt  12939  prmpwdvds  12951  pockthlem  12952  4sqlem11  12997  exmidunben  13070  nninfdclemlt  13095  mulgval  13732  dvdsrtr  14139  dvdsrmul1  14140  unitnegcl  14168  unitpropdg  14186  elrhmunit  14215  zndvds0  14688  znunit  14697  mplsubgfilemcl  14742  psmettri2  15081  ismet2  15107  xmettri2  15114  comet  15252  ivthinclemum  15388  ivthinclemlopn  15389  ivthinclemlr  15390  ivthinclemuopn  15391  ivthinclemur  15392  ivthinclemdisj  15393  ivthinclemloc  15394  ivthinc  15396  ivthreinc  15398  limccl  15412  ellimc3apf  15413  sin0pilem2  15535  pilem3  15536  sincosq1sgn  15579  sincosq2sgn  15580  sincosq4sgn  15582  logltb  15627  logle1b  15645  loglt1b  15646  logbgt0b  15719  wilthlem1  15733  sgmval  15736  dvdsppwf1o  15742  perfect1  15751  lgslem1  15758  lgsval  15762  lgsdilem  15785  lgsne0  15796  gausslemma2dlem1a  15816  gausslemma2dlem1f1o  15818  lgseisenlem1  15828  lgseisenlem2  15829  lgsquadlem1  15835  lgsquadlem2  15836  lgsquadlem3  15837  lgsquad2lem2  15840  m1lgs  15843  2lgslem1a1  15844  2lgslem1a  15846  2lgsoddprmlem2  15864  2lgsoddprmlem3  15869  2sqlem4  15876  2sqlem8a  15880  eupth2lem3lem3fi  16350  eupth2lem3lem6fi  16351  eupth2lem3lem4fi  16353  eupth2lem3lem7fi  16354  eupth2lemsfi  16358  eupth2fi  16359  konigsberglem4  16371