Theorem breq2d 4015

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 4007	. 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 1353   class class class wbr 4003

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  breqtrd  4029  sbcbr1g  4059  pofun  4312  csbfv12g  5551  isorel  5808  isocnv  5811  isotr  5816  caovordig  6039  caovordg  6041  caovord  6045  xporderlem  6231  th3qlem2  6637  phplem3g  6855  supsnti  7003  inflbti  7022  difinfinf  7099  enqdc1  7360  ltanqg  7398  ltmnqg  7399  archnqq  7415  prarloclemarch2  7417  prloc  7489  addnqprllem  7525  addlocprlemgt  7532  appdivnq  7561  mulnqprl  7566  1idprl  7588  ltexprlemloc  7605  caucvgprlemcanl  7642  cauappcvgprlemm  7643  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  cauappcvgprlemlim  7659  cauappcvgpr  7660  archrecnq  7661  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemcl  7674  caucvgprlemladdrl  7676  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  caucvgprpr  7710  ltposr  7761  ltasrg  7768  mulgt0sr  7776  mulextsr1lem  7778  mulextsr1  7779  prsrlt  7785  caucvgsrlemcl  7787  caucvgsrlemfv  7789  caucvgsrlembound  7792  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  caucvgsr  7800  map2psrprg  7803  pitonnlem2  7845  pitonn  7846  recidpipr  7854  axpre-ltadd  7884  axpre-mulgt0  7885  axpre-mulext  7886  axarch  7889  nntopi  7892  axcaucvglemval  7895  axcaucvglemcau  7896  axcaucvglemres  7897  axpre-suploclemres  7899  ltaddneg  8379  ltsubadd2  8388  lesubadd2  8390  ltaddsub  8391  leaddsub  8393  ltaddpos2  8408  posdif  8410  lesub1  8411  ltsub1  8413  ltnegcon1  8418  lenegcon1  8421  addge02  8428  leaddle0  8432  ltordlem  8437  possumd  8524  sublt0d  8525  apreap  8542  prodgt02  8808  prodge02  8810  ltmulgt12  8820  lemulge12  8822  ltdivmul  8831  ledivmul  8832  ltdivmul2  8833  lt2mul2div  8834  ledivmul2  8835  ltrec  8838  ltrec1  8843  ltdiv23  8847  lediv23  8848  nnge1  8940  halfpos  9148  lt2halves  9152  addltmul  9153  avglt2  9156  avgle2  9158  nnrecl  9172  zltlem1  9308  difgtsumgt  9320  nn0le2is012  9333  gtndiv  9346  qapne  9637  nnledivrp  9764  xltnegi  9833  xltadd1  9874  xsubge0  9879  xposdif  9880  xlesubadd  9881  xleaddadd  9885  divelunit  10000  eluzgtdifelfzo  10194  qtri3or  10240  exbtwnzlemstep  10245  exbtwnzlemshrink  10246  exbtwnzlemex  10247  exbtwnz  10248  rebtwn2zlemstep  10250  rebtwn2zlemshrink  10251  rebtwn2z  10252  flqlelt  10273  flqbi  10287  2tnp1ge0ge0  10298  q2submod  10382  frec2uzltd  10400  frec2uzlt2d  10401  frec2uzf1od  10403  monoord  10473  ser3mono  10475  ser3ge0  10514  expnbnd  10640  nn0ltexp2  10685  facwordi  10715  hashunlem  10779  zfz1isolemiso  10814  seq3coll  10817  caucvgrelemcau  10984  caucvgre  10985  cvg1nlemcau  10988  cvg1nlemres  10989  recvguniq  10999  resqrexlemover  11014  resqrexlemgt0  11024  resqrexlemoverl  11025  resqrexlemglsq  11026  resqrexlemsqa  11028  resqrexlemex  11029  maxleastlt  11219  minmax  11233  lemininf  11237  ltmininf  11238  xrmaxleastlt  11259  xrmaxltsup  11261  xrminmax  11268  xrmin1inf  11270  xrmin2inf  11271  xrltmininf  11273  xrlemininf  11274  climserle  11348  summodclem3  11383  summodclem2a  11384  summodc  11386  zsumdc  11387  fsum3  11390  fsum00  11465  fsumabs  11468  cvgratnnlemnexp  11527  cvgratnnlemmn  11528  zproddc  11582  fprodseq  11586  fprodle  11643  sin01bnd  11760  cos01bnd  11761  summodnegmod  11824  modmulconst  11825  dvdsaddr  11839  dvdssub  11840  dvdssubr  11841  dvdslelemd  11843  dvdsfac  11860  dvdsmod  11862  oddp1even  11875  ltoddhalfle  11892  opoe  11894  omoe  11895  divalg2  11925  divalgmod  11926  ndvdssub  11929  ndvdsadd  11930  bezoutlembi  12000  dvdssqim  12019  dvdsmulgcd  12020  dvdssq  12026  nn0seqcvgd  12035  coprmdvds  12086  coprmdvds2  12087  rpmul  12092  cncongr1  12097  divgcdodd  12137  isprm6  12141  prmdvdsexp  12142  prmdvdsexpr  12144  prmfac1  12146  oddpwdclemxy  12163  oddpwdclemodd  12166  sqpweven  12169  2sqpwodd  12170  sqne2sq  12171  hashdvds  12215  phiprmpw  12216  eulerthlemh  12225  prmdiv  12229  prmdiveq  12230  odzval  12235  odzcllem  12236  odzdvds  12239  pythagtriplem11  12268  pythagtriplem13  12270  pythagtrip  12277  pceulem  12288  pczndvds2  12311  pcdvdsb  12313  pc2dvds  12323  pcz  12325  pcprmpw2  12326  dvdsprmpweq  12328  dvdsprmpweqle  12330  difsqpwdvds  12331  pcmpt  12335  prmpwdvds  12347  pockthlem  12348  exmidunben  12421  nninfdclemlt  12446  mulgval  12980  dvdsrtr  13263  dvdsrmul1  13264  unitnegcl  13292  unitpropdg  13310  psmettri2  13759  ismet2  13785  xmettri2  13792  comet  13930  ivthinclemum  14044  ivthinclemlopn  14045  ivthinclemlr  14046  ivthinclemuopn  14047  ivthinclemur  14048  ivthinclemdisj  14049  ivthinclemloc  14050  ivthinc  14052  limccl  14059  ellimc3apf  14060  sin0pilem2  14134  pilem3  14135  sincosq1sgn  14178  sincosq2sgn  14179  sincosq4sgn  14181  logltb  14226  logle1b  14244  loglt1b  14245  logbgt0b  14315  lgslem1  14332  lgsval  14336  lgsdilem  14359  lgsne0  14370  2sqlem4  14385  2sqlem8a  14389