Theorem breq1d 4140

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

Hypothesis

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

Assertion

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

Proof of Theorem breq1d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq1 4133	. 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:  eqnbrtrd  4148  eqbrtrd  4152  eqbrtrdi  4169  sbcbr2g  4188  pofun  4457  fmptco  5874  isorel  6014  isocnv  6017  isotr  6022  imbrov2fvoveq  6110  caovordig  6255  caovordg  6257  caovord  6261  xporderlem  6467  reldmtpos  6524  brtposg  6525  tpostpos  6535  tposoprab  6551  th3qlem2  6912  ensn1g  7084  fndmeng  7098  xpsneng  7120  xpcomco  7124  snnen2oprc  7161  tridc  7204  fimax2gtrilemstep  7205  unsnfidcel  7228  pm54.43  7536  pr1or2  7540  ccfunen  7630  ltsonq  7765  ltanqg  7767  ltmnqg  7768  archnqq  7784  prloc  7858  addnqprulem  7895  appdivnq  7930  mulnqpru  7936  mullocprlem  7937  1idpru  7958  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnbj  8060  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlemexb  8074  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  ltsosr  8131  ltasrg  8137  addgt0sr  8142  mulextsr1  8148  prsrlt  8154  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  ltpsrprg  8170  pitonnlem2  8214  pitonn  8215  recidpipr  8223  axpre-ltadd  8253  axpre-mulext  8255  nntopi  8261  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  ltaddnegr  8753  ltsubadd  8760  lesubadd  8762  ltaddsub2  8765  leaddsub2  8767  ltaddpos  8780  lesub2  8785  ltsub2  8787  ltnegcon2  8792  lenegcon2  8795  addge01  8800  subge0  8803  suble0  8804  lesub0  8807  ltordlem  8810  apreap  8915  divap0b  9013  mulgt1  9193  ltmulgt11  9194  gt0div  9200  ge0div  9201  ltmuldiv  9204  ltmuldiv2  9205  lemuldiv2  9212  ltrec  9213  lerec2  9219  ltdiv23  9222  lediv23  9223  sup3exmid  9287  addltmul  9542  avglt1  9544  avgle1  9546  div4p1lem1div2  9559  ztri3or  9687  zlem1lt  9701  zgt0ge1  9703  qapne  10039  irrmulap  10048  divlt1lt  10125  divle1le  10126  xrltso  10198  xltnegi  10237  xltadd1  10278  xposdif  10284  xlesubadd  10285  xleaddadd  10289  nn0disj  10545  qavgle  10693  fldiv4lem1div2uz2  10741  frec2uzf1od  10843  iseqf1olemfvp  10947  seqf1oglem1  10956  exp3vallem  10977  expap0  11006  leexp2r  11030  sqap0  11043  nn0ltexp2  11147  nn0opthlem1d  11158  hashennnuni  11218  hashunlem  11244  hashf1  11287  zfz1isolemiso  11291  seq3coll  11294  swrdccatin2  11501  shftfvalg  11583  shftfibg  11585  shftfval  11586  shftfib  11588  shftfn  11589  2shfti  11596  shftidt2  11597  caucvgre  11747  cvg1nlemcau  11750  cvg1nlemres  11751  resqrexlemdecn  11778  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemsqa  11790  resqrexlemex  11791  abs00ap  11828  absdiflt  11858  absdifle  11859  lenegsq  11861  cau3lem  11880  minmax  11996  xrmaxltsup  12024  xrminmax  12031  xrltmininf  12036  xrlemininf  12037  clim  12047  clim2  12049  clim0  12051  clim0c  12052  climi0  12055  climuni  12059  2clim  12067  climshftlemg  12068  climshft  12070  climabs0  12073  climcn1  12074  climcn2  12075  addcn2  12076  subcn2  12077  mulcn2  12078  iser3shft  12112  climcau  12113  serf0  12118  sumeq1  12121  sumeq2  12125  sumrbdc  12146  summodclem2  12149  summodc  12150  zsumdc  12151  isumshft  12257  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  prodfap0  12312  prodfrecap  12313  prodfdivap  12314  ntrivcvgap  12315  ntrivcvgap0  12316  prodeq1f  12319  prodeq2w  12323  prodeq2  12324  prodrbdclem2  12340  prodmodclem2  12344  prodmodc  12345  zproddc  12346  fprodntrivap  12351  fprodap0  12388  fprodrec  12396  fproddivapf  12398  fprodap0f  12403  tanaddaplem  12505  sin01bnd  12524  cos01bnd  12525  halfleoddlt  12661  gcddvds  12740  dvdssq  12808  lcmgcdlem  12855  lcmdvds  12857  isprm  12887  prmgt1  12910  isprm5lem  12919  isprm6  12925  pw2dvdslemn  12943  pw2dvdseu  12946  oddpwdclemxy  12947  oddpwdclemndvds  12949  oddpwdclemodd  12950  odzdvds  13024  pclem0  13065  pclemub  13066  pclemdc  13067  pcprecl  13068  pcprendvds  13069  pcpremul  13072  pceulem  13073  pcval  13075  pcelnn  13100  pc2dvds  13109  pcadd  13119  pcadd2  13120  pcmpt  13122  prmpwdvds  13134  4sqlem17  13186  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemodife  13240  ballotfilemic  13250  ballotfilemsv  13253  ballotfilemrc  13274  imasaddfnlemg  13635  znf1o  14986  znidomb  14993  mplsubgfilemm  15089  mplsubgfilemcl  15090  blfvalps  15486  elblps  15491  elbl  15492  elbl3ps  15495  elbl3  15496  blres  15535  comet  15600  bdbl  15604  xmetxp  15608  xmetxpbl  15609  metcnp2  15614  txmetcnp  15619  cnbl0  15635  cnblcld  15636  bl2ioo  15651  addcncntoplem  15662  divcnap  15666  mpomulcn  15667  elcncf  15674  elcncf2  15675  cncfi  15679  rescncf  15682  mulc1cncf  15690  cncfco  15692  cncfmet  15693  cncfmptid  15698  addccncf  15701  cdivcncfap  15705  negcncf  15706  mulcncflem  15708  mulcncf  15709  ivthinclemlm  15735  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemdisj  15741  ivthinclemloc  15742  ivthinc  15744  ivthreinc  15746  limccl  15760  ellimc3apf  15761  limcdifap  15763  limcmpted  15764  limcimolemlt  15765  limcresi  15767  cnplimcim  15768  limccnpcntop  15776  limccnp2lem  15777  limccoap  15779  dvcoapbr  15808  dveflem  15827  eflt  15876  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  logltb  15975  logge0b  15991  loggt0b  15992  pellexlem3  16093  lgslem2  16120  lgslem3  16121  lgsval  16123  lgsfcl2  16125  lgsfle1  16128  lgsle1  16134  lgsdirprm  16153  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem2  16181  gausslemma2dlem3  16182  gausslemma2dlem4  16183  subupgr  16514  vtxdumgrfival  16539  qdencn  17072  trilpolemlt1  17090