Theorem breq12d 5122

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is referenced by:  breq123d  5123  3brtr3d  5142  3brtr4d  5143  sbcbr  5166  pocl  5577  csbcnvgALTOLD  5874  cnvpo  6288  sbcfung  6560  isoeq1  7315  isocnv  7328  isotr  7334  caovordig  7615  caovordg  7617  caovord2d  7619  caovord  7621  ofrfvalg  7682  ofrval  7686  ofrfval2  7695  caofref  7705  fnwelem  8123  poseq  8150  fundmeng  9025  enrefnn  9039  xpsneng  9046  xpcomeng  9053  xpdom2g  9057  limensuc  9138  infensuc  9139  pssnn  9149  unxpdom  9215  dif1ennnALT  9233  unfilem3  9263  fodomfi  9268  domunfican  9277  marypha1lem  9389  infsupprpr  9462  wemaplem1  9504  wemaplem2  9505  wemapwe  9662  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  dmttrcl  9686  rnttrcl  9687  ttrclselem2  9691  dif1card  9990  infxpenlem  9993  nnadju  10177  pwsdompw  10182  infmap2  10196  sornom  10256  isfin5  10278  isfin6  10279  domtriomlem  10421  axdc2lem  10427  axdclem2  10499  pwcfsdom  10563  cfpwsdom  10564  alephom  10565  fpwwe2lem6  10616  fpwwe2lem8  10618  tskcard  10761  ordpipq  10922  adderpqlem  10934  mulerpqlem  10935  mulcanenq  10940  lterpq  10950  ltanq  10951  ltmnq  10952  ltaddnq  10954  ltrnq  10959  archnq  10960  reclem4pr  11030  ltasr  11080  sqgt0sr  11086  axpre-ltadd  11147  axpre-mulgt0  11148  ltadd1  11676  leadd2  11678  ltmul2  12061  lemul2  12063  lemul1a  12064  ltdiv1  12074  ltdiv2  12096  lediv2  12100  div4p1lem1div2  12494  nn0ledivnn  13126  xleadd1  13276  xltadd2  13278  xsubge0  13282  xlemul1a  13309  xlemul1  13311  xlemul2  13312  xltmul2  13314  ltdifltdiv  13863  fzennn  14000  monoord  14064  monoord2  14065  expmordi  14199  ltexp2r  14205  leexp1a  14207  sqlecan  14241  bernneq  14261  faclbnd  14322  faclbnd3  14324  faclbnd4lem1  14325  faclbnd4lem2  14326  faclbnd4lem3  14327  faclbnd4lem4  14328  faclbnd6  14331  facubnd  14332  rlimcld2  15625  isercoll2  15716  climsup  15717  iseraltlem2  15730  fsumabs  15849  fsumrlim  15859  climcndslem1  15899  climcndslem2  15900  supcvg  15906  geomulcvg  15926  cvgrat  15933  ntrivcvgtail  15950  ruclem2  16283  ruclem8  16288  addmodlteqALT  16378  fproddvdsd  16388  sadcaddlem  16510  sadcadd  16511  nn0seqcvgd  16623  algcvg  16629  algcvga  16632  eucalgcvga  16639  isprm5  16761  qnumgt0  16804  pcprendvds2  16896  pcpremul  16898  pcadd2  16945  prmreclem4  16974  prmreclem5  16975  prmreclem6  16976  2expltfac  17147  xpsle  17628  mreexexlemd  17695  issubc  17887  latjlej2  18505  latmlem2  18521  ischn  18658  chnltm1  18660  chnind  18672  chnub  18673  sylow1lem3  19665  isslw  19673  fislw  19690  efgi  19784  lt6abl  19960  ablfac1eu  20140  isomnd  20188  omndadd  20193  omndmul  20200  ogrpinvlt  20209  gsumle  20210  isabv  20914  abvtri  20925  psdmul  22329  cayleyhamilton1  23049  isucn  24434  ispsmet  24461  psmettri2  24466  ismet  24480  isxmet  24481  xmettri2  24497  imasdsf1olem  24530  imasf1oxmet  24532  blvalps  24542  blval  24543  comet  24670  stdbdxmet  24672  nrmmetd  24731  tngngp  24811  tngngp3  24813  nmofval  24871  nmolb2d  24875  nmoi  24885  nmoix  24886  icopnfhmeo  25102  xrhmeo  25105  evth2  25119  pi1grplem  25208  minveclem6  25593  ovolfiniun  25660  ovoliunlem3  25663  voliunlem3  25711  ioombl1  25721  mbfmax  25808  mbfpos  25810  itg1climres  25873  mbfi1fseqlem2  25875  mbfi1fseqlem6  25879  mbfi1fseq  25880  mbfmullem  25884  itg2split  25908  itg2monolem1  25909  itg2monolem3  25911  itg2mono  25912  itg2i1fseqle  25913  itg2i1fseq  25914  itg2i1fseq2  25915  itg2addlem  25917  rolle  26149  dvlip  26152  c1lip1  26156  dvcnvrelem1  26176  dvcvx  26179  ply1divex  26294  q1pval  26312  fta1glem2  26326  fta1g  26327  fta1b  26329  plydivlem3  26456  fta1lem  26468  fta1  26469  aalioulem3  26497  aalioulem4  26498  aaliou3lem2  26506  aaliou3lem8  26508  aaliou3lem9  26513  ulmdvlem1  26563  ulmdvlem3  26565  abelthlem2  26595  abelthlem7a  26600  argrege0  26776  cxplt  26859  cxplea  26861  cxple2  26862  cxplt3  26865  logbleb  26948  logblt  26949  rlimcxp  27138  scvxcvx  27150  jensenlem2  27152  ftalem3  27239  ftalem7  27243  vmalelog  27369  chtub  27376  chpchtsum  27383  bclbnd  27444  efexple  27445  bposlem5  27452  bposlem6  27453  bposlem7  27454  lgsdilem  27488  2lgslem1a2  27554  2sqreuop  27626  2sqreuopnn  27627  2sqreuoplt  27628  2sqreuopltb  27629  2sqreuopnnlt  27630  2sqreuopnnltb  27631  dchrisumlem3  27655  dchrmusumlema  27657  dchrmusum2  27658  dchrvmasumlem2  27662  dchrvmasumlema  27664  dchrvmasumiflem1  27665  dchrisum0flblem2  27673  dchrisum0flb  27674  dchrisum0lema  27678  dchrisum0lem1b  27679  dchrisum0lem2  27682  pntrlog2bndlem2  27742  pntibndlem2  27755  pntlemf  27769  ostth2lem1  27782  qabvle  27789  ltsval2  27820  ltsres  27826  nolesgn2o  27835  nogesgn1o  27837  nodense  27856  nolt02o  27859  nogt01o  27860  noresle  27861  nosupbnd2lem1  27879  nosupbnd2  27880  noinfbnd2lem1  27894  noinfbnd2  27895  addsproplem1  28162  addsprop  28169  ltadds2im  28179  leadds2im  28181  leadds1  28182  leadds2  28183  ltadds1  28185  ltsubs1  28269  ltsubs2  28270  ltsubsubsbd  28276  ltsubsubs2bd  28277  posdifsd  28291  subsge0d  28293  mulsproplemcbv  28308  mulsproplem1  28309  mulsprop  28323  lemulsd  28331  ltmuls1d  28366  ltmulnegs1d  28369  ltmulnegs2d  28370  lemuls1ad  28375  zsoring  28602  pw2gt0divsd  28638  pw2ge0divsd  28639  legso  28868  iscgra  29120  isleag  29164  iseqlg  29184  brbtwn2  29255  axlowdim  29311  ewlksfval  29951  isnvlem  30962  nvtri  31022  nmlnoubi  31148  nmblolbii  31151  nmblolbi  31152  blocnilem  31156  sii  31206  ubthlem2  31223  minvecolem3  31228  minvecolem5  31233  minvecolem6  31234  norm-ii  31490  norm3dif  31502  norm3adifi  31505  bcs  31533  pjnorm  32076  pjnel  32078  nmbdoplbi  32376  nmbdoplb  32377  nmcoplb  32382  lnconi  32385  nmbdfnlb  32402  nmcfnlb  32406  pjdifnormi  32519  mdslmd2i  32682  cvmd  32688  cvexch  32726  cdj1i  32785  cdj3lem1  32786  cdj3lem2b  32789  cdj3lem3b  32792  cdj3i  32793  fnfvor  32954  ofrco  32955  isoun  33047  nexple  33177  ismnt  33303  mgcmntco  33314  dfmgc2lem  33315  dfmgc2  33316  mgcf1o  33323  isinftm  33501  rlocaddval  33589  rlocmulval  33590  fldext2chn  34118  constrextdg2lem  34138  constrext2chn  34149  xrmulc1cn  34320  lmdvg  34343  faeval  34636  brfae  34638  inelcarsg  34701  carsgsigalem  34705  carsgclctunlem2  34709  carsgclctun  34711  hgt750lemc  35034  hgt750lemd  35035  hgt749d  35036  fineqvnttrclse  35537  sconnpht  35721  snmlval  35823  satfv1lem  35854  satfv1  35855  satfv0fun  35863  satfv0fvfmla0  35905  lediv2aALT  36169  faclim  36238  fvtransport  36524  idinside  36576  btwnconn1lem7  36585  btwnconn1lem11  36589  btwnconn1lem12  36590  ditgeq123dv  36753  cbvditgdavw2  36830  nn0prpwlem  36853  weiunval  36993  weiunfrlem  36995  bj-opabco  37852  poimirlem29  38320  heicant  38326  itg2addnclem  38342  itg2addnclem3  38344  itg2gt0cn  38346  ftc1anclem6  38369  ftc1anc  38372  ftc2nc  38373  dvasin  38375  areacirclem1  38379  seqpo  38418  incsequz  38419  metf1o  38426  mettrifi  38428  cntotbnd  38467  heiborlem4  38485  heiborlem6  38487  heiborlem10  38491  bfplem1  38493  bfplem2  38494  isopos  39974  oplecon3b  39994  atlatle  40114  4at2  40408  pmaple  40555  islaut  40877  lautcnvle  40883  lautco  40891  ltrncnvel  40936  cdlemeg49lebilem  41333  cdlemg17h  41462  tendoset  41553  tendotp  41555  cdlemk39s  41733  lcmineqlem23  42838  lcmineqlem  42839  intlewftc  42848  aks4d1p1p4  42858  dvle2  42859  aks4d1p8d2  42872  aks4d1p9  42875  aks4d1  42876  2ap1caineq  42932  sticksstones1  42933  sticksstones2  42934  sticksstones3  42935  sticksstones8  42940  sticksstones10  42942  sticksstones11  42943  sticksstones12a  42944  sticksstones15  42948  aks6d1c7lem3  42969  unitscyglem1  42982  brif12  43016  dvdsexpnn0  43115  dvdsexpb  43116  reltsub1  43167  irrapxlem2  43570  irrapxlem4  43572  irrapxlem5  43573  irrapxlem6  43574  pellexlem3  43578  monotuz  43688  monotoddzzfi  43689  monotoddzz  43690  jm2.17a  43707  jm2.17b  43708  rmygeid  43711  rmydioph  43761  expdiophlem1  43768  expdiophlem2  43769  ttac  43783  fnwe2lem2  43798  relexp01min  44459  cvgdvgrat  45043  relpeq1  45673  monoords  46036  supxrgelem  46073  supxrge  46074  abslt2sqd  46096  ltmulneg  46127  ltdiv23neg  46129  monoordxrv  46215  monoordxr  46216  monoord2xrv  46217  monoord2xr  46218  evthiccabs  46232  sqrlearg  46289  climinf  46342  climinff  46347  limsupres  46439  climinf2  46441  climinf2mpt  46448  climinfmpt  46449  supcnvlimsup  46474  liminfval2  46502  liminfltlem  46538  fprodsubrecnncnvlem  46641  fprodaddrecnncnvlem  46643  ioodvbdlimc1lem1  46665  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  iblspltprt  46707  itgspltprt  46713  stoweidlem3  46737  fourierdlem2  46843  fourierdlem3  46844  fourierdlem11  46852  fourierdlem12  46853  fourierdlem15  46856  fourierdlem34  46875  fourierdlem41  46882  fourierdlem48  46888  fourierdlem49  46889  fourierdlem79  46919  fourierdlem83  46923  fourierdlem89  46929  fourierdlem91  46931  fourierdlem100  46940  fourierdlem107  46947  fourierdlem109  46949  fourierdlem112  46952  etransclem31  46999  etransclem32  47000  rrndistlt  47024  ioorrnopn  47039  ioorrnopnxrlem  47040  sge0less  47126  sge0le  47141  sge0split  47143  sge0lempt  47144  sge0iunmptlemre  47149  sge0isum  47161  sge0seq  47180  meaiuninclem  47214  meaiininclem  47220  meaiininc  47221  isome  47228  omeunile  47239  omeiunlempt  47254  carageniuncllem2  47256  0ome  47263  isomenndlem  47264  isomennd  47265  ovnssle  47295  ovnsubadd  47306  hsphoidmvle2  47319  hsphoidmvle  47320  hoidmvval0  47321  hoidmv1lelem1  47325  hoidmv1lelem2  47326  hoidmv1lelem3  47327  hoidmv1le  47328  hoidmvlelem1  47329  hoidmvlelem2  47330  hoidmvlelem3  47331  hoidmvlelem4  47332  hoidmvlelem5  47333  hoidmvle  47334  hoidifhspdmvle  47354  hspmbllem2  47361  hspmbl  47363  ovnsubadd2lem  47379  ovolval4lem2  47384  ovolval4  47385  ovolval5lem2  47387  vonioolem2  47415  vonioo  47416  vonicclem2  47418  vonicc  47419  smfid  47486  smflimlem3  47507  ormkglobd  47611  natglobalincr  47613  chnerlem1  47618  squeezedltsq  47623  2elfz2melfz  48075  smonoord  48134  iccpart  48185  iccpartimp  48186  iccpartres  48187  sqrtpwpw2p  48310  grlicsym  48798  grlictr  48800  ismgmALT  49008  iscmgmALT  49009  issgrpALT  49010  iscsgrpALT  49011  lindslinindsimp2lem5  49262  rrx2plordisom  49523  aacllem  50641