Theorem breq2d 4142

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
breq2d	⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Proof of Theorem breq2d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq2 4134	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   class class class wbr 4130

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 4131

This theorem is used by:  breqtrd  4156  sbcbr1g  4187  pofun  4457  csbfv12g  5736  isorel  6014  isocnv  6017  isotr  6022  caovordig  6255  caovordg  6257  caovord  6261  xporderlem  6467  th3qlem2  6912  phplem3g  7157  supsnti  7345  inflbti  7364  difinfinf  7441  enqdc1  7729  ltanqg  7767  ltmnqg  7768  archnqq  7784  prarloclemarch2  7786  prloc  7858  addnqprllem  7894  addlocprlemgt  7901  appdivnq  7930  mulnqprl  7935  1idprl  7957  ltexprlemloc  7974  caucvgprlemcanl  8011  cauappcvgprlemm  8012  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  archrecnq  8030  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemcl  8043  caucvgprlemladdrl  8045  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgprpr  8079  ltposr  8130  ltasrg  8137  mulgt0sr  8145  mulextsr1lem  8147  mulextsr1  8148  prsrlt  8154  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsrlembound  8161  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  map2psrprg  8172  pitonnlem2  8214  pitonn  8215  recidpipr  8223  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  axarch  8258  nntopi  8261  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  ltaddneg  8752  ltsubadd2  8761  lesubadd2  8763  ltaddsub  8764  leaddsub  8766  ltaddpos2  8781  posdif  8783  lesub1  8784  ltsub1  8786  ltnegcon1  8791  lenegcon1  8794  addge02  8801  leaddle0  8805  ltordlem  8810  possumd  8897  sublt0d  8898  apreap  8915  prodgt02  9183  prodge02  9185  ltmulgt12  9195  lemulge12  9197  ltdivmul  9206  ledivmul  9207  ltdivmul2  9208  lt2mul2div  9209  ledivmul2  9210  ltrec  9213  ltrec1  9218  ltdiv23  9222  lediv23  9223  nnge1  9327  halfpos  9536  lt2halves  9541  addltmul  9542  avglt2  9545  avgle2  9547  nnrecl  9561  zltlem1  9702  difgtsumgt  9714  nn0le2is012  9728  gtndiv  9741  qapne  10039  nnledivrp  10167  xltnegi  10237  xltadd1  10278  xsubge0  10283  xposdif  10284  xlesubadd  10285  xleaddadd  10289  divelunit  10404  eluzgtdifelfzo  10615  qtri3or  10675  exbtwnzlemstep  10682  exbtwnzlemshrink  10683  exbtwnzlemex  10684  exbtwnz  10685  rebtwn2zlemstep  10687  rebtwn2zlemshrink  10688  rebtwn2z  10689  flqlelt  10711  flqbi  10725  2tnp1ge0ge0  10736  q2submod  10822  frec2uzltd  10840  frec2uzlt2d  10841  frec2uzf1od  10843  monoord  10922  ser3mono  10924  ser3ge0  10973  expnbnd  11101  nn0ltexp2  11147  facwordi  11178  hashunlem  11244  ssenneg  11280  zfz1isolemiso  11291  seq3coll  11294  swrdccat3blem  11511  caucvgrelemcau  11746  caucvgre  11747  cvg1nlemcau  11750  cvg1nlemres  11751  recvguniq  11761  resqrexlemover  11776  resqrexlemgt0  11786  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemsqa  11790  resqrexlemex  11791  maxleastlt  11981  minmax  11996  lemininf  12000  ltmininf  12001  xrmaxleastlt  12022  xrmaxltsup  12024  xrminmax  12031  xrmin1inf  12033  xrmin2inf  12034  xrltmininf  12036  xrlemininf  12037  climserle  12111  summodclem3  12147  summodclem2a  12148  summodc  12150  zsumdc  12151  fsum3  12154  fsum00  12229  fsumabs  12232  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  zproddc  12346  fprodseq  12350  fprodle  12407  sin01bnd  12524  cos01bnd  12525  summodnegmod  12589  modmulconst  12590  dvdsaddr  12604  dvdssub  12605  dvdssubr  12606  dvdslelemd  12610  dvdsfac  12627  dvdsmod  12629  oddp1even  12643  ltoddhalfle  12660  opoe  12662  omoe  12663  divalg2  12693  divalgmod  12694  ndvdssub  12697  ndvdsadd  12698  bitsfval  12709  bitsval  12710  bits0  12715  bitsp1  12718  bitsfzolem  12721  bitsfzo  12722  bitscmp  12725  bitsinv1lem  12728  bezoutlembi  12782  dvdssqim  12801  dvdsmulgcd  12802  dvdssq  12808  nn0seqcvgd  12819  coprmdvds  12870  coprmdvds2  12871  rpmul  12876  cncongr1  12881  divgcdodd  12921  isprm6  12925  prmdvdsexp  12926  prmdvdsexpr  12928  prmfac1  12930  oddpwdclemxy  12947  oddpwdclemodd  12950  sqpweven  12953  2sqpwodd  12954  sqne2sq  12955  hashdvds  12999  phiprmpw  13000  eulerthlemh  13009  prmdiv  13013  prmdiveq  13014  odzval  13020  odzcllem  13021  odzdvds  13024  pythagtriplem11  13053  pythagtriplem13  13055  pythagtrip  13062  pceulem  13073  pczndvds2  13097  pcdvdsb  13099  pc2dvds  13109  pcz  13111  pcprmpw2  13112  dvdsprmpweq  13114  dvdsprmpweqle  13116  difsqpwdvds  13117  pcmpt  13122  prmpwdvds  13134  pockthlem  13135  4sqlem11  13180  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfileme  13236  ballotfilemefi  13237  ballotfilemodife  13240  ballotfilem4  13241  ballotfilem1c  13251  ballotfilemsval  13252  ballotfilemieq  13260  ballotfilemfrcn0  13273  ballotfi  13282  exmidunben  13317  nninfdclemlt  13342  mulgval  13925  dvdsrtr  14408  dvdsrmul1  14409  unitnegcl  14437  unitpropdg  14455  elrhmunit  14484  zndvds0  14985  znunit  14994  mplsubgfilemcl  15090  psmettri2  15429  ismet2  15455  xmettri2  15462  comet  15600  ivthinclemum  15736  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemdisj  15741  ivthinclemloc  15742  ivthinc  15744  ivthreinc  15746  limccl  15760  ellimc3apf  15761  sin0pilem2  15883  pilem3  15884  sincosq1sgn  15927  sincosq2sgn  15928  sincosq4sgn  15930  logltb  15975  logle1b  15993  loglt1b  15994  logbgt0b  16068  wilthlem1  16094  sgmval  16097  dvdsppwf1o  16103  perfect1  16112  lgslem1  16119  lgsval  16123  lgsdilem  16146  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  lgseisenlem1  16189  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem2  16201  m1lgs  16204  2lgslem1a1  16205  2lgslem1a  16207  2lgsoddprmlem2  16225  2lgsoddprmlem3  16230  2sqlem4  16237  2sqlem8a  16241  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  eupth2lem3lem7fi  16715  eupth2lemsfi  16719  eupth2fi  16720  konigsberglem4  16732