Theorem breq2d 4143

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 4135	. 2 |- ( A = B -> ( C R A <-> C R B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C R A <-> C R B ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   class class class wbr 4131

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132

This theorem is used by:  breqtrd  4157  sbcbr1g  4188  pofun  4459  csbfv12g  5739  isorel  6017  isocnv  6020  isotr  6025  caovordig  6258  caovordg  6260  caovord  6264  xporderlem  6471  th3qlem2  6916  phplem3g  7162  supsnti  7352  inflbti  7371  difinfinf  7448  enqdc1  7736  ltanqg  7774  ltmnqg  7775  archnqq  7791  prarloclemarch2  7793  prloc  7865  addnqprllem  7901  addlocprlemgt  7908  appdivnq  7937  mulnqprl  7942  1idprl  7964  ltexprlemloc  7981  caucvgprlemcanl  8018  cauappcvgprlemm  8019  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  cauappcvgprlem1  8033  cauappcvgprlemlim  8035  cauappcvgpr  8036  archrecnq  8037  caucvgprlemnkj  8040  caucvgprlemnbj  8041  caucvgprlemm  8042  caucvgprlemcl  8050  caucvgprlemladdrl  8052  caucvgpr  8056  caucvgprprlemell  8059  caucvgprprlemelu  8060  caucvgprprlemcbv  8061  caucvgprprlemval  8062  caucvgprprlemnkeqj  8064  caucvgprprlemml  8068  caucvgprprlemmu  8069  caucvgprprlemopl  8071  caucvgprprlemlol  8072  caucvgprprlemopu  8073  caucvgprprlemloc  8077  caucvgprprlemclphr  8079  caucvgprprlemexbt  8080  caucvgprprlem1  8083  caucvgprprlem2  8084  caucvgprpr  8086  ltposr  8137  ltasrg  8144  mulgt0sr  8152  mulextsr1lem  8154  mulextsr1  8155  prsrlt  8161  caucvgsrlemcl  8163  caucvgsrlemfv  8165  caucvgsrlembound  8168  caucvgsrlemgt1  8169  caucvgsrlemoffres  8174  caucvgsr  8176  map2psrprg  8179  pitonnlem2  8221  pitonn  8222  recidpipr  8230  axpre-ltadd  8260  axpre-mulgt0  8261  axpre-mulext  8262  axarch  8265  nntopi  8268  axcaucvglemval  8271  axcaucvglemcau  8272  axcaucvglemres  8273  axpre-suploclemres  8275  ltaddneg  8760  ltsubadd2  8769  lesubadd2  8771  ltaddsub  8772  leaddsub  8774  ltaddpos2  8789  posdif  8791  lesub1  8792  ltsub1  8794  ltnegcon1  8799  lenegcon1  8802  addge02  8809  leaddle0  8813  ltordlem  8818  possumd  8906  sublt0d  8907  apreap  8924  prodgt02  9192  prodge02  9194  ltmulgt12  9204  lemulge12  9206  ltdivmul  9215  ledivmul  9216  ltdivmul2  9217  lt2mul2div  9218  ledivmul2  9219  ltrec  9222  ltrec1  9227  ltdiv23  9231  lediv23  9232  nnge1  9337  halfpos  9548  lt2halves  9553  addltmul  9554  avglt2  9557  avgle2  9559  nnrecl  9573  zltlem1  9714  difgtsumgt  9726  nn0le2is012  9740  gtndiv  9753  qapne  10056  nnledivrp  10185  xltnegi  10255  xltadd1  10296  xsubge0  10301  xposdif  10302  xlesubadd  10303  xleaddadd  10307  divelunit  10422  eluzgtdifelfzo  10633  qtri3or  10693  exbtwnzlemstep  10700  exbtwnzlemshrink  10701  exbtwnzlemex  10702  exbtwnz  10703  rebtwn2zlemstep  10705  rebtwn2zlemshrink  10706  rebtwn2z  10707  flqlelt  10730  flaplelt  10731  flqbi  10747  2tnp1ge0ge0  10758  q2submod  10844  frec2uzltd  10862  frec2uzlt2d  10863  frec2uzf1od  10865  monoord  10944  ser3mono  10946  ser3ge0  10995  expnbnd  11123  nn0ltexp2  11170  facwordi  11201  hashunlem  11267  ssenneg  11303  zfz1isolemiso  11314  seq3coll  11317  swrdccat3blem  11534  caucvgrelemcau  11769  caucvgre  11770  cvg1nlemcau  11773  cvg1nlemres  11774  recvguniq  11784  resqrexlemover  11799  resqrexlemgt0  11809  resqrexlemoverl  11810  resqrexlemglsq  11811  resqrexlemsqa  11813  resqrexlemex  11814  maxleastlt  12005  minmax  12021  lemininf  12025  ltmininf  12026  xrmaxleastlt  12048  xrmaxltsup  12050  xrminmax  12057  xrmin1inf  12059  xrmin2inf  12060  xrltmininf  12062  xrlemininf  12063  climserle  12137  summodclem3  12173  summodclem2a  12174  summodc  12176  zsumdc  12177  fsum3  12180  fsum00  12255  fsumabs  12258  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  zproddc  12372  fprodseq  12376  fprodle  12433  sin01bnd  12550  cos01bnd  12551  summodnegmod  12615  modmulconst  12616  dvdsaddr  12630  dvdssub  12631  dvdssubr  12632  dvdslelemd  12636  dvdsfac  12653  dvdsmod  12655  oddp1even  12669  ltoddhalfle  12686  opoe  12688  omoe  12689  divalg2  12719  divalgmod  12720  ndvdssub  12723  ndvdsadd  12724  bitsfval  12735  bitsval  12736  bits0  12741  bitsp1  12744  bitsfzolem  12747  bitsfzo  12748  bitscmp  12751  bitsinv1lem  12754  bezoutlembi  12808  dvdssqim  12827  dvdsmulgcd  12828  dvdssq  12834  nn0seqcvgd  12845  coprmdvds  12896  coprmdvds2  12897  rpmul  12902  cncongr1  12907  divgcdodd  12948  isprm6  12952  prmdvdsexp  12953  prmdvdsexpr  12955  prmfac1  12957  nnmaxpwlemxy  12974  nnmaxpwlemnfac  12977  sqpweven  12981  2sqpwodd  12982  sqne2sq  12983  hashdvds  13029  phiprmpw  13030  eulerthlemh  13039  prmdiv  13043  prmdiveq  13044  odzval  13050  odzcllem  13051  odzdvds  13054  pythagtriplem11  13083  pythagtriplem13  13085  pythagtrip  13092  pceulem  13103  pczndvds2  13127  pcdvdsb  13129  pc2dvds  13139  pcz  13141  pcprmpw2  13142  dvdsprmpweq  13144  dvdsprmpweqle  13146  difsqpwdvds  13147  pcmpt  13152  prmpwdvds  13164  pockthlem  13165  4sqlem11  13210  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfileme  13295  ballotfilemefi  13296  ballotfilemodife  13299  ballotfilem4  13300  ballotfilem1c  13310  ballotfilemsval  13311  ballotfilemieq  13319  ballotfilemfrcn0  13332  ballotfi  13341  exmidunben  13376  nninfdclemlt  13401  mulgval  13985  dvdsrtr  14518  dvdsrmul1  14519  unitnegcl  14547  unitpropdg  14565  elrhmunit  14594  zndvds0  15095  znunit  15104  mplsubgfilemcl  15227  psmettri2  15566  ismet2  15592  xmettri2  15599  comet  15737  ivthinclemum  15873  ivthinclemlopn  15874  ivthinclemlr  15875  ivthinclemuopn  15876  ivthinclemur  15877  ivthinclemdisj  15878  ivthinclemloc  15879  ivthinc  15881  ivthreinc  15883  limccl  15897  ellimc3apf  15898  sin0pilem2  16021  pilem3  16022  sincosq1sgn  16065  sincosq2sgn  16066  sincosq4sgn  16068  logltb  16116  logle1b  16134  loglt1b  16135  logbgt0b  16214  wilthlem1  16244  sgmval  16264  dvdsppwf1o  16295  chtublem  16307  chtqub  16308  perfect1  16310  bcmono  16316  bclbnd  16319  bposlem1  16323  bposlem5  16327  lgslem1  16336  lgsval  16340  lgsdilem  16363  lgsne0  16374  gausslemma2dlem1a  16394  gausslemma2dlem1f1o  16396  lgseisenlem1  16406  lgseisenlem2  16407  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  lgsquad2lem2  16418  m1lgs  16421  2lgslem1a1  16422  2lgslem1a  16424  2lgsoddprmlem2  16442  2lgsoddprmlem3  16447  2sqlem4  16454  2sqlem8a  16458  eupth2lem3lem3fi  16928  eupth2lem3lem6fi  16929  eupth2lem3lem4fi  16931  eupth2lem3lem7fi  16932  eupth2lemsfi  16936  eupth2fi  16937  konigsberglem4  16949