Theorem breq12d 5125

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

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

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 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5113

This theorem is used by:  breq123d  5126  3brtr3d  5145  3brtr4d  5146  sbcbr  5169  pocl  5580  csbcnvgALTOLD  5877  cnvpo  6292  sbcfung  6564  isoeq1  7319  isocnv  7332  isotr  7338  caovordig  7621  caovordg  7623  caovord2d  7625  caovord  7627  ofrfvalg  7688  ofrval  7692  ofrfval2  7701  caofref  7711  fnwelem  8129  poseq  8156  fundmeng  9031  enrefnn  9045  xpsneng  9052  xpcomeng  9059  xpdom2g  9063  limensuc  9144  infensuc  9145  pssnn  9155  unxpdom  9221  dif1ennnALT  9239  unfilem3  9269  fodomfi  9274  domunfican  9283  marypha1lem  9395  infsupprpr  9468  wemaplem1  9510  wemaplem2  9511  wemapwe  9668  ssttrcl  9686  ttrcltr  9687  ttrclss  9691  dmttrcl  9692  rnttrcl  9693  ttrclselem2  9697  dif1card  10005  infxpenlem  10008  nnadju  10192  pwsdompw  10197  infmap2  10211  sornom  10271  isfin5  10293  isfin6  10294  domtriomlem  10436  axdc2lem  10442  axdclem2  10514  pwcfsdom  10578  cfpwsdom  10579  alephom  10580  fpwwe2lem6  10631  fpwwe2lem8  10633  tskcard  10776  ordpipq  10937  adderpqlem  10949  mulerpqlem  10950  mulcanenq  10955  lterpq  10965  ltanq  10966  ltmnq  10967  ltaddnq  10969  ltrnq  10974  archnq  10975  reclem4pr  11045  ltasr  11095  sqgt0sr  11101  axpre-ltadd  11162  axpre-mulgt0  11163  ltadd1  11691  leadd2  11693  ltmul2  12076  lemul2  12078  lemul1a  12079  ltdiv1  12089  ltdiv2  12111  lediv2  12115  div4p1lem1div2  12509  nn0ledivnn  13141  xleadd1  13291  xltadd2  13293  xsubge0  13297  xlemul1a  13324  xlemul1  13326  xlemul2  13327  xltmul2  13329  ltdifltdiv  13878  fzennn  14015  monoord  14079  monoord2  14080  expmordi  14214  ltexp2r  14220  leexp1a  14222  sqlecan  14256  bernneq  14276  faclbnd  14337  faclbnd3  14339  faclbnd4lem1  14340  faclbnd4lem2  14341  faclbnd4lem3  14342  faclbnd4lem4  14343  faclbnd6  14346  facubnd  14347  rlimcld2  15640  isercoll2  15731  climsup  15732  iseraltlem2  15745  fsumabs  15864  fsumrlim  15874  climcndslem1  15914  climcndslem2  15915  supcvg  15921  geomulcvg  15941  cvgrat  15948  ntrivcvgtail  15965  ruclem2  16298  ruclem8  16303  addmodlteqALT  16393  fproddvdsd  16403  sadcaddlem  16525  sadcadd  16526  nn0seqcvgd  16638  algcvg  16644  algcvga  16647  eucalgcvga  16654  isprm5  16776  qnumgt0  16819  pcprendvds2  16911  pcpremul  16913  pcadd2  16960  prmreclem4  16989  prmreclem5  16990  prmreclem6  16991  2expltfac  17162  xpsle  17643  mreexexlemd  17710  issubc  17902  latjlej2  18520  latmlem2  18536  ischn  18673  chnltm1  18675  chnind  18687  chnub  18688  sylow1lem3  19680  isslw  19688  fislw  19705  efgi  19799  lt6abl  19975  ablfac1eu  20155  isomnd  20203  omndadd  20208  omndmul  20215  ogrpinvlt  20224  gsumle  20225  isabv  20929  abvtri  20940  psdmul  22344  cayleyhamilton1  23064  isucn  24449  ispsmet  24476  psmettri2  24481  ismet  24495  isxmet  24496  xmettri2  24512  imasdsf1olem  24545  imasf1oxmet  24547  blvalps  24557  blval  24558  comet  24685  stdbdxmet  24687  nrmmetd  24746  tngngp  24826  tngngp3  24828  nmofval  24886  nmolb2d  24890  nmoi  24900  nmoix  24901  icopnfhmeo  25117  xrhmeo  25120  evth2  25134  pi1grplem  25223  minveclem6  25608  ovolfiniun  25675  ovoliunlem3  25678  voliunlem3  25726  ioombl1  25736  mbfmax  25823  mbfpos  25825  itg1climres  25888  mbfi1fseqlem2  25890  mbfi1fseqlem6  25894  mbfi1fseq  25895  mbfmullem  25899  itg2split  25923  itg2monolem1  25924  itg2monolem3  25926  itg2mono  25927  itg2i1fseqle  25928  itg2i1fseq  25929  itg2i1fseq2  25930  itg2addlem  25932  rolle  26164  dvlip  26167  c1lip1  26171  dvcnvrelem1  26191  dvcvx  26194  ply1divex  26309  q1pval  26327  fta1glem2  26341  fta1g  26342  fta1b  26344  plydivlem3  26471  fta1lem  26483  fta1  26484  aalioulem3  26512  aalioulem4  26513  aaliou3lem2  26521  aaliou3lem8  26523  aaliou3lem9  26528  ulmdvlem1  26578  ulmdvlem3  26580  abelthlem2  26610  abelthlem7a  26615  argrege0  26791  cxplt  26874  cxplea  26876  cxple2  26877  cxplt3  26880  logbleb  26963  logblt  26964  rlimcxp  27153  scvxcvx  27165  jensenlem2  27167  ftalem3  27254  ftalem7  27258  vmalelog  27384  chtub  27391  chpchtsum  27398  bclbnd  27459  efexple  27460  bposlem5  27467  bposlem6  27468  bposlem7  27469  lgsdilem  27503  2lgslem1a2  27569  2sqreuop  27641  2sqreuopnn  27642  2sqreuoplt  27643  2sqreuopltb  27644  2sqreuopnnlt  27645  2sqreuopnnltb  27646  dchrisumlem3  27670  dchrmusumlema  27672  dchrmusum2  27673  dchrvmasumlem2  27677  dchrvmasumlema  27679  dchrvmasumiflem1  27680  dchrisum0flblem2  27688  dchrisum0flb  27689  dchrisum0lema  27693  dchrisum0lem1b  27694  dchrisum0lem2  27697  pntrlog2bndlem2  27757  pntibndlem2  27770  pntlemf  27784  ostth2lem1  27797  qabvle  27804  ltsval2  27835  ltsres  27841  nolesgn2o  27850  nogesgn1o  27852  nodense  27871  nolt02o  27874  nogt01o  27875  noresle  27876  nosupbnd2lem1  27894  nosupbnd2  27895  noinfbnd2lem1  27909  noinfbnd2  27910  addsproplem1  28177  addsprop  28184  ltadds2im  28194  leadds2im  28196  leadds1  28197  leadds2  28198  ltadds1  28200  ltsubs1  28284  ltsubs2  28285  ltsubsubsbd  28291  ltsubsubs2bd  28292  posdifsd  28306  subsge0d  28308  mulsproplemcbv  28323  mulsproplem1  28324  mulsprop  28338  lemulsd  28346  ltmuls1d  28381  ltmulnegs1d  28384  ltmulnegs2d  28385  lemuls1ad  28390  zsoring  28617  pw2gt0divsd  28653  pw2ge0divsd  28654  legso  28883  iscgra  29135  isleag  29179  iseqlg  29199  brbtwn2  29270  axlowdim  29326  ewlksfval  29966  isnvlem  30977  nvtri  31037  nmlnoubi  31163  nmblolbii  31166  nmblolbi  31167  blocnilem  31171  sii  31221  ubthlem2  31238  minvecolem3  31243  minvecolem5  31248  minvecolem6  31249  norm-ii  31505  norm3dif  31517  norm3adifi  31520  bcs  31548  pjnorm  32091  pjnel  32093  nmbdoplbi  32391  nmbdoplb  32392  nmcoplb  32397  lnconi  32400  nmbdfnlb  32417  nmcfnlb  32421  pjdifnormi  32534  mdslmd2i  32697  cvmd  32703  cvexch  32741  cdj1i  32800  cdj3lem1  32801  cdj3lem2b  32804  cdj3lem3b  32807  cdj3i  32808  fnfvor  32969  ofrco  32970  isoun  33062  nexple  33192  ismnt  33316  mgcmntco  33327  dfmgc2lem  33328  dfmgc2  33329  mgcf1o  33336  isinftm  33514  rlocaddval  33602  rlocmulval  33603  fldext2chn  34131  constrextdg2lem  34151  constrext2chn  34162  xrmulc1cn  34333  lmdvg  34356  faeval  34649  brfae  34651  inelcarsg  34714  carsgsigalem  34718  carsgclctunlem2  34722  carsgclctun  34724  hgt750lemc  35047  hgt750lemd  35048  hgt749d  35049  fineqvnttrclse  35549  sconnpht  35733  snmlval  35835  satfv1lem  35866  satfv1  35867  satfv0fun  35875  satfv0fvfmla0  35917  lediv2aALT  36181  faclim  36250  fvtransport  36536  idinside  36588  btwnconn1lem7  36597  btwnconn1lem11  36601  btwnconn1lem12  36602  ditgeq123dv  36765  cbvditgdavw2  36842  nn0prpwlem  36865  weiunval  37005  weiunfrlem  37007  bj-opabco  37864  poimirlem29  38332  heicant  38338  itg2addnclem  38354  itg2addnclem3  38356  itg2gt0cn  38358  ftc1anclem6  38381  ftc1anc  38384  ftc2nc  38385  dvasin  38387  areacirclem1  38391  seqpo  38430  incsequz  38431  metf1o  38438  mettrifi  38440  cntotbnd  38479  heiborlem4  38497  heiborlem6  38499  heiborlem10  38503  bfplem1  38505  bfplem2  38506  isopos  39986  oplecon3b  40006  atlatle  40126  4at2  40420  pmaple  40567  islaut  40889  lautcnvle  40895  lautco  40903  ltrncnvel  40948  cdlemeg49lebilem  41345  cdlemg17h  41474  tendoset  41565  tendotp  41567  cdlemk39s  41745  lcmineqlem23  42850  lcmineqlem  42851  intlewftc  42860  aks4d1p1p4  42870  dvle2  42871  aks4d1p8d2  42884  aks4d1p9  42887  aks4d1  42888  2ap1caineq  42944  sticksstones1  42945  sticksstones2  42946  sticksstones3  42947  sticksstones8  42952  sticksstones10  42954  sticksstones11  42955  sticksstones12a  42956  sticksstones15  42960  aks6d1c7lem3  42981  unitscyglem1  42994  brif12  43028  dvdsexpnn0  43127  dvdsexpb  43128  reltsub1  43179  irrapxlem2  43582  irrapxlem4  43584  irrapxlem5  43585  irrapxlem6  43586  pellexlem3  43590  monotuz  43700  monotoddzzfi  43701  monotoddzz  43702  jm2.17a  43719  jm2.17b  43720  rmygeid  43723  rmydioph  43773  expdiophlem1  43780  expdiophlem2  43781  ttac  43795  fnwe2lem2  43810  relexp01min  44471  cvgdvgrat  45055  relpeq1  45685  monoords  46048  supxrgelem  46085  supxrge  46086  abslt2sqd  46108  ltmulneg  46139  ltdiv23neg  46141  monoordxrv  46227  monoordxr  46228  monoord2xrv  46229  monoord2xr  46230  evthiccabs  46244  sqrlearg  46301  climinf  46354  climinff  46359  limsupres  46451  climinf2  46453  climinf2mpt  46460  climinfmpt  46461  supcnvlimsup  46486  liminfval2  46514  liminfltlem  46550  fprodsubrecnncnvlem  46653  fprodaddrecnncnvlem  46655  ioodvbdlimc1lem1  46677  ioodvbdlimc1lem2  46678  ioodvbdlimc2lem  46680  iblspltprt  46719  itgspltprt  46725  stoweidlem3  46749  fourierdlem2  46855  fourierdlem3  46856  fourierdlem11  46864  fourierdlem12  46865  fourierdlem15  46868  fourierdlem34  46887  fourierdlem41  46894  fourierdlem48  46900  fourierdlem49  46901  fourierdlem79  46931  fourierdlem83  46935  fourierdlem89  46941  fourierdlem91  46943  fourierdlem100  46952  fourierdlem107  46959  fourierdlem109  46961  fourierdlem112  46964  etransclem31  47011  etransclem32  47012  rrndistlt  47036  ioorrnopn  47051  ioorrnopnxrlem  47052  sge0less  47138  sge0le  47153  sge0split  47155  sge0lempt  47156  sge0iunmptlemre  47161  sge0isum  47173  sge0seq  47192  meaiuninclem  47226  meaiininclem  47232  meaiininc  47233  isome  47240  omeunile  47251  omeiunlempt  47266  carageniuncllem2  47268  0ome  47275  isomenndlem  47276  isomennd  47277  ovnssle  47307  ovnsubadd  47318  hsphoidmvle2  47331  hsphoidmvle  47332  hoidmvval0  47333  hoidmv1lelem1  47337  hoidmv1lelem2  47338  hoidmv1lelem3  47339  hoidmv1le  47340  hoidmvlelem1  47341  hoidmvlelem2  47342  hoidmvlelem3  47343  hoidmvlelem4  47344  hoidmvlelem5  47345  hoidmvle  47346  hoidifhspdmvle  47366  hspmbllem2  47373  hspmbl  47375  ovnsubadd2lem  47391  ovolval4lem2  47396  ovolval4  47397  ovolval5lem2  47399  vonioolem2  47427  vonioo  47428  vonicclem2  47430  vonicc  47431  smfid  47498  smflimlem3  47519  ormkglobd  47623  natglobalincr  47625  chnerlem1  47630  squeezedltsq  47635  2elfz2melfz  48087  smonoord  48146  iccpart  48197  iccpartimp  48198  iccpartres  48199  sqrtpwpw2p  48322  grlicsym  48810  grlictr  48812  ismgmALT  49020  iscmgmALT  49021  issgrpALT  49022  iscsgrpALT  49023  lindslinindsimp2lem5  49274  rrx2plordisom  49535  aacllem  50653