Theorem breq12d 5124

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 5116	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  breq123d  5125  3brtr3d  5144  3brtr4d  5145  sbcbr  5168  pocl  5579  csbcnvgALTOLD  5876  cnvpo  6292  sbcfung  6564  isoeq1  7324  isocnv  7337  isotr  7343  caovordig  7625  caovordg  7627  caovord2d  7629  caovord  7631  ofrfvalg  7692  ofrval  7696  ofrfval2  7705  caofref  7715  fnwelem  8133  poseq  8160  fundmeng  9036  enrefnn  9050  xpsneng  9057  xpcomeng  9064  xpdom2g  9068  limensuc  9149  infensuc  9150  pssnn  9160  unxpdom  9226  dif1ennnALT  9244  unfilem3  9274  fodomfi  9279  domunfican  9288  marypha1lem  9400  infsupprpr  9473  wemaplem1  9515  wemaplem2  9516  wemapwe  9673  ssttrcl  9691  ttrcltr  9692  ttrclss  9696  dmttrcl  9697  rnttrcl  9698  ttrclselem2  9702  dif1card  10010  infxpenlem  10013  nnadju  10197  pwsdompw  10202  infmap2  10216  sornom  10276  isfin5  10298  isfin6  10299  domtriomlem  10441  axdc2lem  10447  axdclem2  10519  pwcfsdom  10585  cfpwsdom  10586  alephom  10587  fpwwe2lem6  10638  fpwwe2lem8  10640  tskcard  10783  ordpipq  10944  adderpqlem  10956  mulerpqlem  10957  mulcanenq  10962  lterpq  10972  ltanq  10973  ltmnq  10974  ltaddnq  10976  ltrnq  10981  archnq  10982  reclem4pr  11052  ltasr  11102  sqgt0sr  11108  axpre-ltadd  11169  axpre-mulgt0  11170  ltadd1  11698  leadd2  11700  ltmul2  12083  lemul2  12085  lemul1a  12086  ltdiv1  12096  ltdiv2  12118  lediv2  12122  div4p1lem1div2  12516  nn0ledivnn  13149  xleadd1  13299  xltadd2  13301  xsubge0  13305  xlemul1a  13332  xlemul1  13334  xlemul2  13335  xltmul2  13337  ltdifltdiv  13887  fzennn  14024  monoord  14088  monoord2  14089  expmordi  14223  ltexp2r  14229  leexp1a  14231  sqlecan  14265  bernneq  14285  faclbnd  14346  faclbnd3  14348  faclbnd4lem1  14349  faclbnd4lem2  14350  faclbnd4lem3  14351  faclbnd4lem4  14352  faclbnd6  14355  facubnd  14356  rlimcld2  15655  isercoll2  15746  climsup  15747  iseraltlem2  15760  fsumabs  15878  fsumrlim  15888  climcndslem1  15928  climcndslem2  15929  supcvg  15935  geomulcvg  15955  cvgrat  15962  ntrivcvgtail  15979  ruclem2  16312  ruclem8  16317  addmodlteqALT  16407  fproddvdsd  16417  sadcaddlem  16539  sadcadd  16540  nn0seqcvgd  16652  algcvg  16658  algcvga  16661  eucalgcvga  16668  isprm5  16790  qnumgt0  16833  pcprendvds2  16925  pcpremul  16927  pcadd2  16974  prmreclem4  17003  prmreclem5  17004  prmreclem6  17005  2expltfac  17176  xpsle  17657  mreexexlemd  17724  issubc  17916  latjlej2  18534  latmlem2  18550  ischn  18687  chnltm1  18689  chnind  18701  chnub  18702  sylow1lem3  19716  isslw  19724  fislw  19741  efgi  19835  lt6abl  20011  ablfac1eu  20191  isomnd  20239  omndadd  20244  omndmul  20251  ogrpinvlt  20260  gsumle  20261  isabv  20966  abvtri  20977  psdmul  22381  cayleyhamilton1  23101  isucn  24487  ispsmet  24514  psmettri2  24519  ismet  24533  isxmet  24534  xmettri2  24550  imasdsf1olem  24583  imasf1oxmet  24585  blvalps  24595  blval  24596  comet  24723  stdbdxmet  24725  nrmmetd  24784  tngngp  24864  tngngp3  24866  nmofval  24924  nmolb2d  24928  nmoi  24938  nmoix  24939  icopnfhmeo  25155  xrhmeo  25158  evth2  25172  pi1grplem  25261  minveclem6  25646  ovolfiniun  25713  ovoliunlem3  25716  voliunlem3  25764  ioombl1  25774  mbfmax  25861  mbfpos  25863  itg1climres  25926  mbfi1fseqlem2  25928  mbfi1fseqlem6  25932  mbfi1fseq  25933  mbfmullem  25937  itg2split  25961  itg2monolem1  25962  itg2monolem3  25964  itg2mono  25965  itg2i1fseqle  25966  itg2i1fseq  25967  itg2i1fseq2  25968  itg2addlem  25970  rolle  26202  dvlip  26205  c1lip1  26209  dvcnvrelem1  26229  dvcvx  26232  ply1divex  26347  q1pval  26365  fta1glem2  26379  fta1g  26380  fta1b  26382  plydivlem3  26509  fta1lem  26521  fta1  26522  aalioulem3  26550  aalioulem4  26551  aaliou3lem2  26559  aaliou3lem8  26561  aaliou3lem9  26566  ulmdvlem1  26616  ulmdvlem3  26618  abelthlem2  26648  abelthlem7a  26653  argrege0  26829  cxplt  26912  cxplea  26914  cxple2  26915  cxplt3  26918  logbleb  27001  logblt  27002  rlimcxp  27191  scvxcvx  27203  jensenlem2  27205  ftalem3  27292  ftalem7  27296  vmalelog  27422  chtub  27429  chpchtsum  27436  bclbnd  27497  efexple  27498  bposlem5  27505  bposlem6  27506  bposlem7  27507  lgsdilem  27541  2lgslem1a2  27607  2sqreuop  27679  2sqreuopnn  27680  2sqreuoplt  27681  2sqreuopltb  27682  2sqreuopnnlt  27683  2sqreuopnnltb  27684  dchrisumlem3  27708  dchrmusumlema  27710  dchrmusum2  27711  dchrvmasumlem2  27715  dchrvmasumlema  27717  dchrvmasumiflem1  27718  dchrisum0flblem2  27726  dchrisum0flb  27727  dchrisum0lema  27731  dchrisum0lem1b  27732  dchrisum0lem2  27735  pntrlog2bndlem2  27795  pntibndlem2  27808  pntlemf  27822  ostth2lem1  27835  qabvle  27842  ltsval2  27873  ltsres  27879  nolesgn2o  27888  nogesgn1o  27890  nodense  27909  nolt02o  27912  nogt01o  27913  noresle  27914  nosupbnd2lem1  27932  nosupbnd2  27933  noinfbnd2lem1  27947  noinfbnd2  27948  addsproplem1  28215  addsprop  28222  ltadds2im  28232  leadds2im  28234  leadds1  28235  leadds2  28236  ltadds1  28238  ltsubs1  28322  ltsubs2  28323  ltsubsubsbd  28329  ltsubsubs2bd  28330  posdifsd  28344  subsge0d  28346  mulsproplemcbv  28361  mulsproplem1  28362  mulsprop  28376  lemulsd  28384  ltmuls1d  28419  ltmulnegs1d  28422  ltmulnegs2d  28423  lemuls1ad  28428  zsoring  28655  pw2gt0divsd  28691  pw2ge0divsd  28692  legso  28921  iscgra  29173  isleag  29221  iseqlg  29241  brbtwn2  29312  axlowdim  29368  ewlksfval  30011  isnvlem  31035  nvtri  31095  nmlnoubi  31221  nmblolbii  31224  nmblolbi  31225  blocnilem  31229  sii  31279  ubthlem2  31296  minvecolem3  31301  minvecolem5  31306  minvecolem6  31307  norm-ii  31563  norm3dif  31575  norm3adifi  31578  bcs  31606  pjnorm  32149  pjnel  32151  nmbdoplbi  32449  nmbdoplb  32450  nmcoplb  32455  lnconi  32458  nmbdfnlb  32475  nmcfnlb  32479  pjdifnormi  32592  mdslmd2i  32755  cvmd  32761  cvexch  32799  cdj1i  32858  cdj3lem1  32859  cdj3lem2b  32862  cdj3lem3b  32865  cdj3i  32866  fnfvor  33027  ofrco  33028  isoun  33120  nexple  33249  ismnt  33369  mgcmntco  33380  dfmgc2lem  33381  dfmgc2  33382  mgcf1o  33389  isinftm  33567  rlocaddval  33655  rlocmulval  33656  fldext2chn  34184  constrextdg2lem  34204  constrext2chn  34215  xrmulc1cn  34386  lmdvg  34409  faeval  34703  brfae  34705  inelcarsg  34768  carsgsigalem  34772  carsgclctunlem2  34776  carsgclctun  34778  hgt750lemc  35101  hgt750lemd  35102  hgt749d  35103  fineqvnttrclse  35596  sconnpht  35760  snmlval  35862  satfv1lem  35893  satfv1  35894  satfv0fun  35902  satfv0fvfmla0  35944  lediv2aALT  36208  faclim  36277  fvtransport  36563  idinside  36615  btwnconn1lem7  36624  btwnconn1lem11  36628  btwnconn1lem12  36629  ditgeq123dv  36792  cbvditgdavw2  36869  nn0prpwlem  36892  weiunval  37032  weiunfrlem  37034  bj-opabco  37891  poimirlem29  38359  heicant  38365  itg2addnclem  38381  itg2addnclem3  38383  itg2gt0cn  38385  ftc1anclem6  38408  ftc1anc  38411  ftc2nc  38412  dvasin  38414  areacirclem1  38418  seqpo  38458  incsequz  38459  metf1o  38466  mettrifi  38468  cntotbnd  38507  heiborlem4  38525  heiborlem6  38527  heiborlem10  38531  bfplem1  38533  bfplem2  38534  isopos  40014  oplecon3b  40034  atlatle  40154  4at2  40448  pmaple  40595  islaut  40917  lautcnvle  40923  lautco  40931  ltrncnvel  40976  cdlemeg49lebilem  41373  cdlemg17h  41502  tendoset  41593  tendotp  41595  cdlemk39s  41773  lcmineqlem23  42878  lcmineqlem  42879  intlewftc  42888  aks4d1p1p4  42898  dvle2  42899  aks4d1p8d2  42912  aks4d1p9  42915  aks4d1  42916  2ap1caineq  42972  sticksstones1  42973  sticksstones2  42974  sticksstones3  42975  sticksstones8  42980  sticksstones10  42982  sticksstones11  42983  sticksstones12a  42984  sticksstones15  42988  aks6d1c7lem3  43009  unitscyglem1  43022  brif12  43056  dvdsexpnn0  43155  dvdsexpb  43156  reltsub1  43207  irrapxlem2  43610  irrapxlem4  43612  irrapxlem5  43613  irrapxlem6  43614  pellexlem3  43618  monotuz  43728  monotoddzzfi  43729  monotoddzz  43730  jm2.17a  43747  jm2.17b  43748  rmygeid  43751  rmydioph  43801  expdiophlem1  43808  expdiophlem2  43809  ttac  43823  fnwe2lem2  43838  relexp01min  44499  cvgdvgrat  45083  relpeq1  45713  monoords  46076  supxrgelem  46113  supxrge  46114  abslt2sqd  46136  ltmulneg  46167  ltdiv23neg  46169  monoordxrv  46255  monoordxr  46256  monoord2xrv  46257  monoord2xr  46258  evthiccabs  46272  sqrlearg  46329  climinf  46382  climinff  46387  limsupres  46479  climinf2  46481  climinf2mpt  46488  climinfmpt  46489  supcnvlimsup  46514  liminfval2  46542  liminfltlem  46578  fprodsubrecnncnvlem  46681  fprodaddrecnncnvlem  46683  ioodvbdlimc1lem1  46705  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  iblspltprt  46747  itgspltprt  46753  stoweidlem3  46777  fourierdlem2  46883  fourierdlem3  46884  fourierdlem11  46892  fourierdlem12  46893  fourierdlem15  46896  fourierdlem34  46915  fourierdlem41  46922  fourierdlem48  46928  fourierdlem49  46929  fourierdlem79  46959  fourierdlem83  46963  fourierdlem89  46969  fourierdlem91  46971  fourierdlem100  46980  fourierdlem107  46987  fourierdlem109  46989  fourierdlem112  46992  etransclem31  47039  etransclem32  47040  rrndistlt  47064  ioorrnopn  47079  ioorrnopnxrlem  47080  sge0less  47166  sge0le  47181  sge0split  47183  sge0lempt  47184  sge0iunmptlemre  47189  sge0isum  47201  sge0seq  47220  meaiuninclem  47254  meaiininclem  47260  meaiininc  47261  isome  47268  omeunile  47279  omeiunlempt  47294  carageniuncllem2  47296  0ome  47303  isomenndlem  47304  isomennd  47305  ovnssle  47335  ovnsubadd  47346  hsphoidmvle2  47359  hsphoidmvle  47360  hoidmvval0  47361  hoidmv1lelem1  47365  hoidmv1lelem2  47366  hoidmv1lelem3  47367  hoidmv1le  47368  hoidmvlelem1  47369  hoidmvlelem2  47370  hoidmvlelem3  47371  hoidmvlelem4  47372  hoidmvlelem5  47373  hoidmvle  47374  hoidifhspdmvle  47394  hspmbllem2  47401  hspmbl  47403  ovnsubadd2lem  47419  ovolval4lem2  47424  ovolval4  47425  ovolval5lem2  47427  vonioolem2  47455  vonioo  47456  vonicclem2  47458  vonicc  47459  smfid  47526  smflimlem3  47547  ormkglobd  47651  natglobalincr  47653  chnerlem1  47658  squeezedltsq  47663  2elfz2melfz  48115  smonoord  48174  iccpart  48225  iccpartimp  48226  iccpartres  48227  sqrtpwpw2p  48350  grlicsym  48838  grlictr  48840  ismgmALT  49047  iscmgmALT  49048  issgrpALT  49049  iscsgrpALT  49050  lindslinindsimp2lem5  49301  rrx2plordisom  49562  aacllem  50680