Theorem breq12d 5116

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Hypotheses

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
breq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

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

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		breq12 5108	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  breq123d  5117  3brtr3d  5136  3brtr4d  5137  sbcbr  5160  pocl  5567  csbcnvgALTOLD  5866  cnvpo  6290  sbcfungOLD  6564  isoeq1  7325  isocnv  7338  isotr  7344  caovordig  7626  caovordg  7628  caovord2d  7630  caovord  7632  ofrfvalg  7701  ofrval  7705  ofrfval2  7714  caofref  7724  fnwelem  8143  fnwe2lem3  8147  poseq  8175  fundmeng  9060  enrefnn  9074  xpsneng  9081  xpcomeng  9088  xpdom2g  9092  limensuc  9173  infensuc  9174  pssnn  9184  unxpdom  9250  dif1ennnALT  9268  unfilem3  9299  fodomfi  9304  domunfican  9313  marypha1lem  9425  infsupprpr  9498  wemaplem1  9540  wemaplem2  9541  wemapwe  9698  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  dmttrcl  9722  rnttrcl  9723  ttrclselem2  9727  dif1card  10089  infxpenlem  10092  nnadju  10276  pwsdompw  10281  infmap2  10295  sornom  10355  isfin5  10377  isfin6  10378  domtriomlem  10520  axdc2lem  10526  axdclem2  10598  pwcfsdom  10668  cfpwsdom  10669  alephom  10670  fpwwe2lem6  10721  fpwwe2lem8  10723  tskcard  10866  ordpipq  11027  adderpqlem  11039  mulerpqlem  11040  mulcanenq  11045  lterpq  11055  ltanq  11056  ltmnq  11057  ltaddnq  11059  ltrnq  11064  archnq  11065  reclem4pr  11135  ltasr  11185  sqgt0sr  11191  axpre-ltadd  11252  axpre-mulgt0  11253  ltadd1  11783  leadd2  11785  ltmul2  12168  lemul2  12170  lemul1a  12171  ltdiv1  12181  ltdiv2  12203  lediv2  12207  div4p1lem1div2  12601  nn0ledivnn  13235  xleadd1  13385  xltadd2  13387  xsubge0  13391  xlemul1a  13418  xlemul1  13420  xlemul2  13421  xltmul2  13423  ltdifltdiv  13974  fzennn  14111  monoord  14175  monoord2  14176  expmordi  14310  ltexp2r  14316  leexp1a  14318  sqlecan  14353  bernneq  14373  faclbnd  14434  faclbnd3  14436  faclbnd4lem1  14437  faclbnd4lem2  14438  faclbnd4lem3  14439  faclbnd4lem4  14440  faclbnd6  14443  facubnd  14444  rlimcld2  15745  isercoll2  15836  climsup  15837  iseraltlem2  15850  fsumabs  15968  fsumrlim  15978  climcndslem1  16018  climcndslem2  16019  supcvg  16025  geomulcvg  16045  cvgrat  16052  ntrivcvgtail  16069  ruclem2  16400  ruclem8  16405  addmodlteqALT  16495  fproddvdsd  16505  sadcaddlem  16627  sadcadd  16628  nn0seqcvgd  16745  algcvg  16751  algcvga  16754  eucalgcvga  16761  isprm5  16883  qnumgt0  16926  pcprendvds2  17019  pcpremul  17021  pcadd2  17068  prmreclem4  17097  prmreclem5  17098  prmreclem6  17099  2expltfac  17270  xpsle  17751  mreexexlemd  17818  issubc  18010  latjlej2  18628  latmlem2  18644  ischn  18781  chnltm1  18783  chnind  18795  chnub  18796  sylow1lem3  19814  isslw  19822  fislw  19839  efgi  19933  lt6abl  20109  ablfac1eu  20289  isomnd  20337  omndadd  20342  omndmul  20349  ogrpinvlt  20358  gsumle  20359  isabv  21068  abvtri  21079  psdmul  22487  cayleyhamilton1  23210  isucn  24596  ispsmet  24623  psmettri2  24628  ismet  24642  isxmet  24643  xmettri2  24659  imasdsf1olem  24692  imasf1oxmet  24694  blvalps  24704  blval  24705  comet  24832  stdbdxmet  24834  nrmmetd  24893  tngngp  24973  tngngp3  24975  nmofval  25033  nmolb2d  25037  nmoi  25047  nmoix  25048  icopnfhmeo  25264  xrhmeo  25267  evth2  25281  pi1grplem  25370  minveclem6  25755  ovolfiniun  25822  ovoliunlem3  25825  voliunlem3  25873  ioombl1  25883  mbfmax  25970  mbfpos  25972  itg1climres  26035  mbfi1fseqlem2  26037  mbfi1fseqlem6  26041  mbfi1fseq  26042  mbfmullem  26046  itg2split  26070  itg2monolem1  26071  itg2monolem3  26073  itg2mono  26074  itg2i1fseqle  26075  itg2i1fseq  26076  itg2i1fseq2  26077  itg2addlem  26079  rolle  26310  dvlip  26313  c1lip1  26317  dvcnvrelem1  26337  dvcvx  26340  ply1divex  26455  q1pval  26473  fta1glem2  26487  fta1g  26488  fta1b  26490  plydivlem3  26616  fta1lem  26628  fta1  26629  aalioulem3  26661  aalioulem4  26662  aaliou3lem2  26670  aaliou3lem8  26672  aaliou3lem9  26677  ulmdvlem1  26727  ulmdvlem3  26729  abelthlem2  26759  abelthlem7a  26764  argrege0  26939  cxplt  27022  cxplea  27024  cxple2  27025  cxplt3  27028  logbleb  27111  logblt  27112  rlimcxp  27301  scvxcvx  27313  jensenlem2  27315  ftalem3  27402  ftalem7  27406  vmalelog  27532  chtub  27539  chpchtsum  27546  bclbnd  27607  efexple  27608  bposlem5  27615  bposlem6  27616  bposlem7  27617  lgsdilem  27651  2lgslem1a2  27717  2sqreuop  27789  2sqreuopnn  27790  2sqreuoplt  27791  2sqreuopltb  27792  2sqreuopnnlt  27793  2sqreuopnnltb  27794  dchrisumlem3  27818  dchrmusumlema  27820  dchrmusum2  27821  dchrvmasumlem2  27825  dchrvmasumlema  27827  dchrvmasumiflem1  27828  dchrisum0flblem2  27836  dchrisum0flb  27837  dchrisum0lema  27841  dchrisum0lem1b  27842  dchrisum0lem2  27845  pntrlog2bndlem2  27905  pntibndlem2  27918  pntlemf  27932  ostth2lem1  27945  qabvle  27952  ltsval2  28013  ltsres  28019  nolesgn2o  28028  nogesgn1o  28030  nodense  28049  nolt02o  28052  nogt01o  28053  noresle  28054  nosupbnd2lem1  28072  nosupbnd2  28073  noinfbnd2lem1  28087  noinfbnd2  28088  addsproplem1  28355  addsprop  28362  ltadds2im  28372  leadds2im  28374  leadds1  28375  leadds2  28376  ltadds1  28378  ltsubs1  28462  ltsubs2  28463  ltsubsubsbd  28469  ltsubsubs2bd  28470  posdifsd  28484  subsge0d  28486  mulsproplemcbv  28501  mulsproplem1  28502  mulsprop  28516  lemulsd  28524  ltmuls1d  28559  ltmulnegs1d  28562  ltmulnegs2d  28563  lemuls1ad  28568  zsoring  28795  pw2gt0divsd  28831  pw2ge0divsd  28832  legso  29062  iscgra  29316  isleag  29366  angmgmaddov2  29389  iseqlg  29412  brbtwn2  29483  axlowdim  29539  ewlksfval  30182  isnvlem  31212  nvtri  31272  nmlnoubi  31398  nmblolbii  31401  nmblolbi  31402  blocnilem  31406  sii  31456  ubthlem2  31473  minvecolem3  31478  minvecolem5  31483  minvecolem6  31484  norm-ii  31740  norm3dif  31752  norm3adifi  31755  bcs  31783  pjnorm  32326  pjnel  32328  nmbdoplbi  32626  nmbdoplb  32627  nmcoplb  32632  lnconi  32635  nmbdfnlb  32652  nmcfnlb  32656  pjdifnormi  32769  mdslmd2i  32932  cvmd  32938  cvexch  32976  cdj1i  33035  cdj3lem1  33036  cdj3lem2b  33039  cdj3lem3b  33042  cdj3i  33043  fnfvor  33203  ofrco  33204  isoun  33295  nexple  33424  ismnt  33544  mgcmntco  33555  dfmgc2lem  33556  dfmgc2  33557  mgcf1o  33564  isinftm  33742  rlocaddval  33830  rlocmulval  33831  fldext2chn  34360  constrextdg2lem  34380  constrext2chn  34391  xrmulc1cn  34562  lmdvg  34585  faeval  34879  brfae  34881  inelcarsg  34943  carsgsigalem  34947  carsgclctunlem2  34951  carsgclctun  34953  hgt750lemc  35276  hgt750lemd  35277  hgt749d  35278  fineqvnttrclse  35792  sconnpht  35994  snmlval  36096  satfv1lem  36127  satfv1  36128  satfv0fun  36136  satfv0fvfmla0  36178  lediv2aALT  36442  faclim  36511  fvtransport  36797  idinside  36849  btwnconn1lem7  36858  btwnconn1lem11  36862  btwnconn1lem12  36863  ditgeq123dv  37010  cbvditgdavw2  37087  nn0prpwlem  37110  weiunval  37250  weiunfrlem  37252  bj-opabco  38109  poimirlem29  38567  heicant  38573  itg2addnclem  38589  itg2addnclem3  38591  itg2gt0cn  38593  ftc1anclem6  38616  ftc1anc  38619  ftc2nc  38620  dvasin  38622  areacirclem1  38626  seqpo  38681  incsequz  38682  metf1o  38689  mettrifi  38691  cntotbnd  38730  heiborlem4  38748  heiborlem6  38750  heiborlem10  38754  bfplem1  38756  bfplem2  38757  isopos  40237  oplecon3b  40257  atlatle  40377  4at2  40671  pmaple  40818  islaut  41140  lautcnvle  41146  lautco  41154  ltrncnvel  41199  cdlemeg49lebilem  41596  cdlemg17h  41725  tendoset  41816  tendotp  41818  cdlemk39s  41996  lcmineqlem23  43101  lcmineqlem  43102  intlewftc  43111  aks4d1p1p4  43121  dvle2  43122  aks4d1p8d2  43135  aks4d1p9  43138  aks4d1  43139  2ap1caineq  43195  sticksstones1  43196  sticksstones2  43197  sticksstones3  43198  sticksstones8  43203  sticksstones10  43205  sticksstones11  43206  sticksstones12a  43207  sticksstones15  43211  aks6d1c7lem3  43232  unitscyglem1  43245  brif12  43279  dvdsexpnn0  43386  dvdsexpb  43387  reltsub1  43437  irrapxlem2  43829  irrapxlem4  43831  irrapxlem5  43832  irrapxlem6  43833  pellexlem3  43837  monotuz  43947  monotoddzzfi  43948  monotoddzz  43949  jm2.17a  43966  jm2.17b  43967  rmygeid  43970  rmydioph  44020  expdiophlem1  44027  expdiophlem2  44028  ttac  44042  relexp01min  44712  cvgdvgrat  45296  relpeq1  45933  monoords  46312  supxrgelem  46348  supxrge  46349  abslt2sqd  46371  ltmulneg  46402  ltdiv23neg  46404  monoordxrv  46490  monoordxr  46491  monoord2xrv  46492  monoord2xr  46493  evthiccabs  46507  sqrlearg  46564  climinf  46617  climinff  46622  limsupres  46714  climinf2  46716  climinf2mpt  46723  climinfmpt  46724  supcnvlimsup  46749  liminfval2  46777  liminfltlem  46813  fprodsubrecnncnvlem  46916  fprodaddrecnncnvlem  46918  ioodvbdlimc1lem1  46940  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  iblspltprt  46982  itgspltprt  46988  stoweidlem3  47012  fourierdlem2  47118  fourierdlem3  47119  fourierdlem11  47127  fourierdlem12  47128  fourierdlem15  47131  fourierdlem34  47150  fourierdlem41  47157  fourierdlem48  47163  fourierdlem49  47164  fourierdlem79  47194  fourierdlem83  47198  fourierdlem89  47204  fourierdlem91  47206  fourierdlem100  47215  fourierdlem107  47222  fourierdlem109  47224  fourierdlem112  47227  etransclem31  47274  etransclem32  47275  rrndistlt  47299  ioorrnopn  47314  ioorrnopnxrlem  47315  sge0less  47401  sge0le  47416  sge0split  47418  sge0lempt  47419  sge0iunmptlemre  47424  sge0isum  47436  sge0seq  47455  meaiuninclem  47489  meaiininclem  47495  meaiininc  47496  isome  47503  omeunile  47514  omeiunlempt  47529  carageniuncllem2  47531  0ome  47538  isomenndlem  47539  isomennd  47540  ovnssle  47570  ovnsubadd  47581  hsphoidmvle2  47594  hsphoidmvle  47595  hoidmvval0  47596  hoidmv1lelem1  47600  hoidmv1lelem2  47601  hoidmv1lelem3  47602  hoidmv1le  47603  hoidmvlelem1  47604  hoidmvlelem2  47605  hoidmvlelem3  47606  hoidmvlelem4  47607  hoidmvlelem5  47608  hoidmvle  47609  hoidifhspdmvle  47629  hspmbllem2  47636  hspmbl  47638  ovnsubadd2lem  47654  ovolval4lem2  47659  ovolval4  47660  ovolval5lem2  47662  vonioolem2  47690  vonioo  47691  vonicclem2  47693  vonicc  47694  smfid  47761  smflimlem3  47782  ormkglobd  47886  chnerlem1  47891  squeezedltsq  47911  2elfz2melfz  48387  smonoord  48446  iccpart  48497  iccpartimp  48498  iccpartres  48499  sqrtpwpw2p  48622  grlicsym  49110  grlictr  49112  ismgmALT  49319  iscmgmALT  49320  issgrpALT  49321  iscsgrpALT  49322  lindslinindsimp2lem5  49573  rrx2plordisom  49834  aacllem  50938