Theorem breq2d 4123

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 4115	. 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 1398   class class class wbr 4111

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112

This theorem is referenced by:  breqtrd  4137  sbcbr1g  4168  pofun  4435  csbfv12g  5712  isorel  5983  isocnv  5986  isotr  5991  caovordig  6222  caovordg  6224  caovord  6228  xporderlem  6429  th3qlem2  6874  phplem3g  7112  supsnti  7298  inflbti  7317  difinfinf  7394  enqdc1  7682  ltanqg  7720  ltmnqg  7721  archnqq  7737  prarloclemarch2  7739  prloc  7811  addnqprllem  7847  addlocprlemgt  7854  appdivnq  7883  mulnqprl  7888  1idprl  7910  ltexprlemloc  7927  caucvgprlemcanl  7964  cauappcvgprlemm  7965  cauappcvgprlemladdru  7976  cauappcvgprlemladdrl  7977  cauappcvgprlem1  7979  cauappcvgprlemlim  7981  cauappcvgpr  7982  archrecnq  7983  caucvgprlemnkj  7986  caucvgprlemnbj  7987  caucvgprlemm  7988  caucvgprlemcl  7996  caucvgprlemladdrl  7998  caucvgpr  8002  caucvgprprlemell  8005  caucvgprprlemelu  8006  caucvgprprlemcbv  8007  caucvgprprlemval  8008  caucvgprprlemnkeqj  8010  caucvgprprlemml  8014  caucvgprprlemmu  8015  caucvgprprlemopl  8017  caucvgprprlemlol  8018  caucvgprprlemopu  8019  caucvgprprlemloc  8023  caucvgprprlemclphr  8025  caucvgprprlemexbt  8026  caucvgprprlem1  8029  caucvgprprlem2  8030  caucvgprpr  8032  ltposr  8083  ltasrg  8090  mulgt0sr  8098  mulextsr1lem  8100  mulextsr1  8101  prsrlt  8107  caucvgsrlemcl  8109  caucvgsrlemfv  8111  caucvgsrlembound  8114  caucvgsrlemgt1  8115  caucvgsrlemoffres  8120  caucvgsr  8122  map2psrprg  8125  pitonnlem2  8167  pitonn  8168  recidpipr  8176  axpre-ltadd  8206  axpre-mulgt0  8207  axpre-mulext  8208  axarch  8211  nntopi  8214  axcaucvglemval  8217  axcaucvglemcau  8218  axcaucvglemres  8219  axpre-suploclemres  8221  ltaddneg  8703  ltsubadd2  8712  lesubadd2  8714  ltaddsub  8715  leaddsub  8717  ltaddpos2  8732  posdif  8734  lesub1  8735  ltsub1  8737  ltnegcon1  8742  lenegcon1  8745  addge02  8752  leaddle0  8756  ltordlem  8761  possumd  8848  sublt0d  8849  apreap  8866  prodgt02  9132  prodge02  9134  ltmulgt12  9144  lemulge12  9146  ltdivmul  9155  ledivmul  9156  ltdivmul2  9157  lt2mul2div  9158  ledivmul2  9159  ltrec  9162  ltrec1  9167  ltdiv23  9171  lediv23  9172  nnge1  9265  halfpos  9474  lt2halves  9479  addltmul  9480  avglt2  9483  avgle2  9485  nnrecl  9499  zltlem1  9640  difgtsumgt  9652  nn0le2is012  9666  gtndiv  9679  qapne  9977  nnledivrp  10105  xltnegi  10174  xltadd1  10215  xsubge0  10220  xposdif  10221  xlesubadd  10222  xleaddadd  10226  divelunit  10341  eluzgtdifelfzo  10549  qtri3or  10607  exbtwnzlemstep  10614  exbtwnzlemshrink  10615  exbtwnzlemex  10616  exbtwnz  10617  rebtwn2zlemstep  10619  rebtwn2zlemshrink  10620  rebtwn2z  10621  flqlelt  10643  flqbi  10657  2tnp1ge0ge0  10668  q2submod  10754  frec2uzltd  10772  frec2uzlt2d  10773  frec2uzf1od  10775  monoord  10854  ser3mono  10856  ser3ge0  10905  expnbnd  11033  nn0ltexp2  11079  facwordi  11110  hashunlem  11176  ssenneg  11212  zfz1isolemiso  11219  seq3coll  11222  swrdccat3blem  11439  caucvgrelemcau  11673  caucvgre  11674  cvg1nlemcau  11677  cvg1nlemres  11678  recvguniq  11688  resqrexlemover  11703  resqrexlemgt0  11713  resqrexlemoverl  11714  resqrexlemglsq  11715  resqrexlemsqa  11717  resqrexlemex  11718  maxleastlt  11908  minmax  11923  lemininf  11927  ltmininf  11928  xrmaxleastlt  11949  xrmaxltsup  11951  xrminmax  11958  xrmin1inf  11960  xrmin2inf  11961  xrltmininf  11963  xrlemininf  11964  climserle  12038  summodclem3  12074  summodclem2a  12075  summodc  12077  zsumdc  12078  fsum3  12081  fsum00  12156  fsumabs  12159  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  zproddc  12273  fprodseq  12277  fprodle  12334  sin01bnd  12451  cos01bnd  12452  summodnegmod  12516  modmulconst  12517  dvdsaddr  12531  dvdssub  12532  dvdssubr  12533  dvdslelemd  12537  dvdsfac  12554  dvdsmod  12556  oddp1even  12570  ltoddhalfle  12587  opoe  12589  omoe  12590  divalg2  12620  divalgmod  12621  ndvdssub  12624  ndvdsadd  12625  bitsfval  12636  bitsval  12637  bits0  12642  bitsp1  12645  bitsfzolem  12648  bitsfzo  12649  bitscmp  12652  bitsinv1lem  12655  bezoutlembi  12709  dvdssqim  12728  dvdsmulgcd  12729  dvdssq  12735  nn0seqcvgd  12746  coprmdvds  12797  coprmdvds2  12798  rpmul  12803  cncongr1  12808  divgcdodd  12848  isprm6  12852  prmdvdsexp  12853  prmdvdsexpr  12855  prmfac1  12857  oddpwdclemxy  12874  oddpwdclemodd  12877  sqpweven  12880  2sqpwodd  12881  sqne2sq  12882  hashdvds  12926  phiprmpw  12927  eulerthlemh  12936  prmdiv  12940  prmdiveq  12941  odzval  12947  odzcllem  12948  odzdvds  12951  pythagtriplem11  12980  pythagtriplem13  12982  pythagtrip  12989  pceulem  13000  pczndvds2  13024  pcdvdsb  13026  pc2dvds  13036  pcz  13038  pcprmpw2  13039  dvdsprmpweq  13041  dvdsprmpweqle  13043  difsqpwdvds  13044  pcmpt  13049  prmpwdvds  13061  pockthlem  13062  4sqlem11  13107  ballotfilemfc0  13157  ballotfilemfcc  13158  ballotfileme  13161  ballotfilemodife  13162  ballotfilem4  13163  exmidunben  13198  nninfdclemlt  13223  mulgval  13860  dvdsrtr  14268  dvdsrmul1  14269  unitnegcl  14297  unitpropdg  14315  elrhmunit  14344  zndvds0  14847  znunit  14856  mplsubgfilemcl  14903  psmettri2  15242  ismet2  15268  xmettri2  15275  comet  15413  ivthinclemum  15549  ivthinclemlopn  15550  ivthinclemlr  15551  ivthinclemuopn  15552  ivthinclemur  15553  ivthinclemdisj  15554  ivthinclemloc  15555  ivthinc  15557  ivthreinc  15559  limccl  15573  ellimc3apf  15574  sin0pilem2  15696  pilem3  15697  sincosq1sgn  15740  sincosq2sgn  15741  sincosq4sgn  15743  logltb  15788  logle1b  15806  loglt1b  15807  logbgt0b  15880  wilthlem1  15897  sgmval  15900  dvdsppwf1o  15906  perfect1  15915  lgslem1  15922  lgsval  15926  lgsdilem  15949  lgsne0  15960  gausslemma2dlem1a  15980  gausslemma2dlem1f1o  15982  lgseisenlem1  15992  lgseisenlem2  15993  lgsquadlem1  15999  lgsquadlem2  16000  lgsquadlem3  16001  lgsquad2lem2  16004  m1lgs  16007  2lgslem1a1  16008  2lgslem1a  16010  2lgsoddprmlem2  16028  2lgsoddprmlem3  16033  2sqlem4  16040  2sqlem8a  16044  eupth2lem3lem3fi  16514  eupth2lem3lem6fi  16515  eupth2lem3lem4fi  16517  eupth2lem3lem7fi  16518  eupth2lemsfi  16522  eupth2fi  16523  konigsberglem4  16535