Theorem breq12d 5118

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106

This theorem is used by:  breq123d  5119  3brtr3d  5138  3brtr4d  5139  sbcbr  5163  pocl  5570  csbcnvgALTOLD  5870  cnvpo  6296  sbcfungOLD  6572  isoeq1  7332  isocnv  7345  isotr  7351  caovordig  7633  caovordg  7635  caovord2d  7637  caovord  7639  ofrfvalg  7708  ofrval  7712  ofrfval2  7721  caofref  7731  fnwelem  8153  fnwe2lem3  8157  poseq  8185  fundmeng  9071  enrefnn  9085  xpsneng  9092  xpcomeng  9099  xpdom2g  9103  limensuc  9184  infensuc  9185  pssnn  9195  unxpdom  9261  dif1ennnALT  9279  unfilem3  9310  fodomfi  9315  domunfican  9324  marypha1lem  9435  infsupprpr  9508  wemaplem1  9550  wemaplem2  9551  wemapwe  9708  ssttrcl  9726  ttrcltr  9727  ttrclss  9731  dmttrcl  9732  rnttrcl  9733  ttrclselem2  9737  dif1card  10099  infxpenlem  10102  nnadju  10286  pwsdompw  10291  infmap2  10305  sornom  10365  isfin5  10387  isfin6  10388  domtriomlem  10530  axdc2lem  10536  axdclem2  10608  pwcfsdom  10678  cfpwsdom  10679  alephom  10680  fpwwe2lem6  10731  fpwwe2lem8  10733  tskcard  10876  ordpipq  11037  adderpqlem  11049  mulerpqlem  11050  mulcanenq  11055  lterpq  11065  ltanq  11066  ltmnq  11067  ltaddnq  11069  ltrnq  11074  archnq  11075  reclem4pr  11145  ltasr  11195  sqgt0sr  11201  axpre-ltadd  11262  axpre-mulgt0  11263  ltadd1  11793  leadd2  11795  ltmul2  12178  lemul2  12180  lemul1a  12181  ltdiv1  12191  ltdiv2  12213  lediv2  12217  div4p1lem1div2  12611  nn0ledivnn  13245  xleadd1  13395  xltadd2  13397  xsubge0  13401  xlemul1a  13428  xlemul1  13430  xlemul2  13431  xltmul2  13433  ltdifltdiv  13984  fzennn  14121  monoord  14185  monoord2  14186  expmordi  14320  ltexp2r  14326  leexp1a  14328  sqlecan  14363  bernneq  14383  faclbnd  14444  faclbnd3  14446  faclbnd4lem1  14447  faclbnd4lem2  14448  faclbnd4lem3  14449  faclbnd4lem4  14450  faclbnd6  14453  facubnd  14454  rlimcld2  15757  isercoll2  15848  climsup  15849  iseraltlem2  15862  fsumabs  15980  fsumrlim  15990  climcndslem1  16030  climcndslem2  16031  supcvg  16037  geomulcvg  16057  cvgrat  16064  ntrivcvgtail  16081  ruclem2  16412  ruclem8  16417  addmodlteqALT  16507  fproddvdsd  16517  sadcaddlem  16639  sadcadd  16640  nn0seqcvgd  16757  algcvg  16763  algcvga  16766  eucalgcvga  16773  isprm5  16895  qnumgt0  16938  pcprendvds2  17031  pcpremul  17033  pcadd2  17080  prmreclem4  17109  prmreclem5  17110  prmreclem6  17111  2expltfac  17282  xpsle  17763  mreexexlemd  17830  issubc  18022  latjlej2  18640  latmlem2  18656  ischn  18793  chnltm1  18795  chnind  18807  chnub  18808  sylow1lem3  19826  isslw  19834  fislw  19851  efgi  19945  lt6abl  20121  ablfac1eu  20301  isomnd  20349  omndadd  20354  omndmul  20361  ogrpinvlt  20370  gsumle  20371  isabv  21080  abvtri  21091  psdmul  22499  cayleyhamilton1  23222  isucn  24608  ispsmet  24635  psmettri2  24640  ismet  24654  isxmet  24655  xmettri2  24671  imasdsf1olem  24704  imasf1oxmet  24706  blvalps  24716  blval  24717  comet  24844  stdbdxmet  24846  nrmmetd  24905  tngngp  24985  tngngp3  24987  nmofval  25045  nmolb2d  25049  nmoi  25059  nmoix  25060  icopnfhmeo  25276  xrhmeo  25279  evth2  25293  pi1grplem  25382  minveclem6  25767  ovolfiniun  25834  ovoliunlem3  25837  voliunlem3  25885  ioombl1  25895  mbfmax  25982  mbfpos  25984  itg1climres  26047  mbfi1fseqlem2  26049  mbfi1fseqlem6  26053  mbfi1fseq  26054  mbfmullem  26058  itg2split  26082  itg2monolem1  26083  itg2monolem3  26085  itg2mono  26086  itg2i1fseqle  26087  itg2i1fseq  26088  itg2i1fseq2  26089  itg2addlem  26091  rolle  26322  dvlip  26325  c1lip1  26329  dvcnvrelem1  26349  dvcvx  26352  ply1divex  26467  q1pval  26485  fta1glem2  26499  fta1g  26500  fta1b  26502  plydivlem3  26628  fta1lem  26640  fta1  26641  aalioulem3  26673  aalioulem4  26674  aaliou3lem2  26682  aaliou3lem8  26684  aaliou3lem9  26689  ulmdvlem1  26739  ulmdvlem3  26741  abelthlem2  26771  abelthlem7a  26776  argrege0  26951  cxplt  27034  cxplea  27036  cxple2  27037  cxplt3  27040  logbleb  27123  logblt  27124  rlimcxp  27313  scvxcvx  27325  jensenlem2  27327  ftalem3  27414  ftalem7  27418  vmalelog  27544  chtub  27551  chpchtsum  27558  bclbnd  27619  efexple  27620  bposlem5  27627  bposlem6  27628  bposlem7  27629  lgsdilem  27663  2lgslem1a2  27729  2sqreuop  27801  2sqreuopnn  27802  2sqreuoplt  27803  2sqreuopltb  27804  2sqreuopnnlt  27805  2sqreuopnnltb  27806  dchrisumlem3  27830  dchrmusumlema  27832  dchrmusum2  27833  dchrvmasumlem2  27837  dchrvmasumlema  27839  dchrvmasumiflem1  27840  dchrisum0flblem2  27848  dchrisum0flb  27849  dchrisum0lema  27853  dchrisum0lem1b  27854  dchrisum0lem2  27857  pntrlog2bndlem2  27917  pntibndlem2  27930  pntlemf  27944  ostth2lem1  27957  qabvle  27964  ltsval2  28025  ltsres  28031  nolesgn2o  28040  nogesgn1o  28042  nodense  28061  nolt02o  28064  nogt01o  28065  noresle  28066  nosupbnd2lem1  28084  nosupbnd2  28085  noinfbnd2lem1  28099  noinfbnd2  28100  addsproplem1  28367  addsprop  28374  ltadds2im  28384  leadds2im  28386  leadds1  28387  leadds2  28388  ltadds1  28390  ltsubs1  28474  ltsubs2  28475  ltsubsubsbd  28481  ltsubsubs2bd  28482  posdifsd  28496  subsge0d  28498  mulsproplemcbv  28513  mulsproplem1  28514  mulsprop  28528  lemulsd  28536  ltmuls1d  28571  ltmulnegs1d  28574  ltmulnegs2d  28575  lemuls1ad  28580  zsoring  28807  pw2gt0divsd  28843  pw2ge0divsd  28844  legso  29074  iscgra  29328  isleag  29378  angmgmaddov2  29401  iseqlg  29424  brbtwn2  29495  axlowdim  29551  ewlksfval  30194  isnvlem  31224  nvtri  31284  nmlnoubi  31410  nmblolbii  31413  nmblolbi  31414  blocnilem  31418  sii  31468  ubthlem2  31485  minvecolem3  31490  minvecolem5  31495  minvecolem6  31496  norm-ii  31752  norm3dif  31764  norm3adifi  31767  bcs  31795  pjnorm  32338  pjnel  32340  nmbdoplbi  32638  nmbdoplb  32639  nmcoplb  32644  lnconi  32647  nmbdfnlb  32664  nmcfnlb  32668  pjdifnormi  32781  mdslmd2i  32944  cvmd  32950  cvexch  32988  cdj1i  33047  cdj3lem1  33048  cdj3lem2b  33051  cdj3lem3b  33054  cdj3i  33055  fnfvor  33257  ofrco  33258  isoun  33349  nexple  33477  ismnt  33597  mgcmntco  33608  dfmgc2lem  33609  dfmgc2  33610  mgcf1o  33617  isinftm  33795  rlocaddval  33883  rlocmulval  33884  fldext2chn  34413  constrextdg2lem  34433  constrext2chn  34444  xrmulc1cn  34615  lmdvg  34638  faeval  34932  brfae  34934  inelcarsg  34996  carsgsigalem  35000  carsgclctunlem2  35004  carsgclctun  35006  hgt750lemc  35329  hgt750lemd  35330  hgt749d  35331  fineqvnttrclse  35863  sconnpht  36115  snmlval  36217  satfv1lem  36248  satfv1  36249  satfv0fun  36257  satfv0fvfmla0  36299  lediv2aALT  36563  faclim  36638  fvtransport  36924  idinside  36976  btwnconn1lem7  36985  btwnconn1lem11  36989  btwnconn1lem12  36990  ditgeq123dv  37137  cbvditgdavw2  37214  nn0prpwlem  37237  weiunval  37377  weiunfrlem  37379  bj-opabco  38249  poimirlem29  38707  heicant  38713  itg2addnclem  38729  itg2addnclem3  38731  itg2gt0cn  38733  ftc1anclem6  38756  ftc1anc  38759  ftc2nc  38760  dvasin  38762  areacirclem1  38766  seqpo  38821  incsequz  38822  metf1o  38829  mettrifi  38831  cntotbnd  38870  heiborlem4  38888  heiborlem6  38890  heiborlem10  38894  bfplem1  38896  bfplem2  38897  isopos  40377  oplecon3b  40397  atlatle  40517  4at2  40811  pmaple  40958  islaut  41280  lautcnvle  41286  lautco  41294  ltrncnvel  41339  cdlemeg49lebilem  41736  cdlemg17h  41865  tendoset  41956  tendotp  41958  cdlemk39s  42136  lcmineqlem23  43241  lcmineqlem  43242  intlewftc  43251  aks4d1p1p4  43261  dvle2  43262  aks4d1p8d2  43275  aks4d1p9  43278  aks4d1  43279  2ap1caineq  43335  sticksstones1  43336  sticksstones2  43337  sticksstones3  43338  sticksstones8  43343  sticksstones10  43345  sticksstones11  43346  sticksstones12a  43347  sticksstones15  43351  aks6d1c7lem3  43372  unitscyglem1  43385  brif12  43419  dvdsexpnn0  43526  dvdsexpb  43527  reltsub1  43577  irrapxlem2  43970  irrapxlem4  43972  irrapxlem5  43973  irrapxlem6  43974  pellexlem3  43978  monotuz  44088  monotoddzzfi  44089  monotoddzz  44090  jm2.17a  44107  jm2.17b  44108  rmygeid  44111  rmydioph  44161  expdiophlem1  44168  expdiophlem2  44169  ttac  44183  relexp01min  44853  cvgdvgrat  45437  relpeq1  46073  monoords  46452  supxrgelem  46488  supxrge  46489  abslt2sqd  46511  ltmulneg  46542  ltdiv23neg  46544  monoordxrv  46630  monoordxr  46631  monoord2xrv  46632  monoord2xr  46633  evthiccabs  46647  sqrlearg  46704  climinf  46757  climinff  46762  limsupres  46854  climinf2  46856  climinf2mpt  46863  climinfmpt  46864  supcnvlimsup  46889  liminfval2  46917  liminfltlem  46953  fprodsubrecnncnvlem  47056  fprodaddrecnncnvlem  47058  ioodvbdlimc1lem1  47080  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  iblspltprt  47122  itgspltprt  47128  stoweidlem3  47152  fourierdlem2  47258  fourierdlem3  47259  fourierdlem11  47267  fourierdlem12  47268  fourierdlem15  47271  fourierdlem34  47290  fourierdlem41  47297  fourierdlem48  47303  fourierdlem49  47304  fourierdlem79  47334  fourierdlem83  47338  fourierdlem89  47344  fourierdlem91  47346  fourierdlem100  47355  fourierdlem107  47362  fourierdlem109  47364  fourierdlem112  47367  etransclem31  47414  etransclem32  47415  rrndistlt  47439  ioorrnopn  47454  ioorrnopnxrlem  47455  sge0less  47541  sge0le  47556  sge0split  47558  sge0lempt  47559  sge0iunmptlemre  47564  sge0isum  47576  sge0seq  47595  meaiuninclem  47629  meaiininclem  47635  meaiininc  47636  isome  47643  omeunile  47654  omeiunlempt  47669  carageniuncllem2  47671  0ome  47678  isomenndlem  47679  isomennd  47680  ovnssle  47710  ovnsubadd  47721  hsphoidmvle2  47734  hsphoidmvle  47735  hoidmvval0  47736  hoidmv1lelem1  47740  hoidmv1lelem2  47741  hoidmv1lelem3  47742  hoidmv1le  47743  hoidmvlelem1  47744  hoidmvlelem2  47745  hoidmvlelem3  47746  hoidmvlelem4  47747  hoidmvlelem5  47748  hoidmvle  47749  hoidifhspdmvle  47769  hspmbllem2  47776  hspmbl  47778  ovnsubadd2lem  47794  ovolval4lem2  47799  ovolval4  47800  ovolval5lem2  47802  vonioolem2  47830  vonioo  47831  vonicclem2  47833  vonicc  47834  smfid  47901  smflimlem3  47922  ormkglobd  48026  chnerlem1  48031  squeezedltsq  48051  2elfz2melfz  48527  smonoord  48586  iccpart  48637  iccpartimp  48638  iccpartres  48639  sqrtpwpw2p  48762  grlicsym  49250  grlictr  49252  ismgmALT  49459  iscmgmALT  49460  issgrpALT  49461  iscsgrpALT  49462  lindslinindsimp2lem5  49713  rrx2plordisom  49975  aacllem  51153