Theorem breq12d 5098

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  breq123d  5099  3brtr3d  5116  3brtr4d  5117  sbcbr  5140  pocl  5547  csbcnvgALT  5839  cnvpo  6251  sbcfung  6522  isoeq1  7272  isocnv  7285  isotr  7291  caovordig  7572  caovordg  7574  caovord2d  7576  caovord  7578  ofrfvalg  7639  ofrval  7643  ofrfval2  7652  caofref  7662  fnwelem  8081  poseq  8108  fundmeng  8979  enrefnn  8993  xpsneng  9000  xpcomeng  9007  xpdom2g  9011  limensuc  9092  infensuc  9093  pssnn  9103  unxpdom  9169  dif1ennnALT  9187  unfilem3  9217  fodomfi  9222  domunfican  9232  fodomfiOLD  9240  marypha1lem  9346  infsupprpr  9419  wemaplem1  9461  wemaplem2  9462  wemapwe  9618  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  dmttrcl  9642  rnttrcl  9643  ttrclselem2  9647  dif1card  9932  infxpenlem  9935  nnadju  10120  pwsdompw  10125  infmap2  10139  sornom  10199  isfin5  10221  isfin6  10222  domtriomlem  10364  axdc2lem  10370  axdclem2  10442  pwcfsdom  10506  cfpwsdom  10507  alephom  10508  fpwwe2lem6  10559  fpwwe2lem8  10561  tskcard  10704  ordpipq  10865  adderpqlem  10877  mulerpqlem  10878  mulcanenq  10883  lterpq  10893  ltanq  10894  ltmnq  10895  ltaddnq  10897  ltrnq  10902  archnq  10903  reclem4pr  10973  ltasr  11023  sqgt0sr  11029  axpre-ltadd  11090  axpre-mulgt0  11091  ltadd1  11617  leadd2  11619  ltmul2  12006  lemul2  12008  lemul1a  12009  ltdiv1  12020  ltdiv2  12042  lediv2  12046  div4p1lem1div2  12432  nn0ledivnn  13057  xleadd1  13207  xltadd2  13209  xsubge0  13213  xlemul1a  13240  xlemul1  13242  xlemul2  13243  xltmul2  13245  ltdifltdiv  13793  fzennn  13930  monoord  13994  monoord2  13995  expmordi  14129  ltexp2r  14135  leexp1a  14137  sqlecan  14171  bernneq  14191  faclbnd  14252  faclbnd3  14254  faclbnd4lem1  14255  faclbnd4lem2  14256  faclbnd4lem3  14257  faclbnd4lem4  14258  faclbnd6  14261  facubnd  14262  rlimcld2  15540  isercoll2  15631  climsup  15632  iseraltlem2  15645  fsumabs  15764  fsumrlim  15774  climcndslem1  15814  climcndslem2  15815  supcvg  15821  geomulcvg  15841  cvgrat  15848  ntrivcvgtail  15865  ruclem2  16199  ruclem8  16204  addmodlteqALT  16294  fproddvdsd  16304  sadcaddlem  16426  sadcadd  16427  nn0seqcvgd  16539  algcvg  16545  algcvga  16548  eucalgcvga  16555  isprm5  16677  qnumgt0  16720  pcprendvds2  16812  pcpremul  16814  pcadd2  16861  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  2expltfac  17063  xpsle  17543  mreexexlemd  17610  issubc  17802  latjlej2  18420  latmlem2  18436  ischn  18573  chnltm1  18575  chnind  18587  chnub  18588  sylow1lem3  19575  isslw  19583  fislw  19600  efgi  19694  lt6abl  19870  ablfac1eu  20050  isomnd  20098  omndadd  20103  omndmul  20110  ogrpinvlt  20119  gsumle  20120  isabv  20788  abvtri  20799  psdmul  22132  cayleyhamilton1  22857  isucn  24242  ispsmet  24269  psmettri2  24274  ismet  24288  isxmet  24289  xmettri2  24305  imasdsf1olem  24338  imasf1oxmet  24340  blvalps  24350  blval  24351  comet  24478  stdbdxmet  24480  nrmmetd  24539  tngngp  24619  tngngp3  24621  nmofval  24679  nmolb2d  24683  nmoi  24693  nmoix  24694  icopnfhmeo  24910  xrhmeo  24913  evth2  24927  pi1grplem  25016  minveclem6  25401  ovolfiniun  25468  ovoliunlem3  25471  voliunlem3  25519  ioombl1  25529  mbfmax  25616  mbfpos  25618  itg1climres  25681  mbfi1fseqlem2  25683  mbfi1fseqlem6  25687  mbfi1fseq  25688  mbfmullem  25692  itg2split  25716  itg2monolem1  25717  itg2monolem3  25719  itg2mono  25720  itg2i1fseqle  25721  itg2i1fseq  25722  itg2i1fseq2  25723  itg2addlem  25725  rolle  25957  dvlip  25960  c1lip1  25964  dvcnvrelem1  25984  dvcvx  25987  ply1divex  26102  q1pval  26120  fta1glem2  26134  fta1g  26135  fta1b  26137  plydivlem3  26261  fta1lem  26273  fta1  26274  aalioulem3  26300  aalioulem4  26301  aaliou3lem2  26309  aaliou3lem8  26311  aaliou3lem9  26316  ulmdvlem1  26365  ulmdvlem3  26367  abelthlem2  26397  abelthlem7a  26402  argrege0  26575  cxplt  26658  cxplea  26660  cxple2  26661  cxplt3  26664  logbleb  26747  logblt  26748  rlimcxp  26937  scvxcvx  26949  jensenlem2  26951  ftalem3  27038  ftalem7  27042  vmalelog  27168  chtub  27175  chpchtsum  27182  bclbnd  27243  efexple  27244  bposlem5  27251  bposlem6  27252  bposlem7  27253  lgsdilem  27287  2lgslem1a2  27353  2sqreuop  27425  2sqreuopnn  27426  2sqreuoplt  27427  2sqreuopltb  27428  2sqreuopnnlt  27429  2sqreuopnnltb  27430  dchrisumlem3  27454  dchrmusumlema  27456  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumlema  27463  dchrvmasumiflem1  27464  dchrisum0flblem2  27472  dchrisum0flb  27473  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem2  27481  pntrlog2bndlem2  27541  pntibndlem2  27554  pntlemf  27568  ostth2lem1  27581  qabvle  27588  ltsval2  27620  ltsres  27626  nolesgn2o  27635  nogesgn1o  27637  nodense  27656  nolt02o  27659  nogt01o  27660  noresle  27661  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd2lem1  27694  noinfbnd2  27695  addsproplem1  27961  addsprop  27968  ltadds2im  27978  leadds2im  27980  leadds1  27981  leadds2  27982  ltadds1  27984  ltsubs1  28068  ltsubs2  28069  ltsubsubsbd  28075  ltsubsubs2bd  28076  posdifsd  28090  subsge0d  28092  mulsproplemcbv  28107  mulsproplem1  28108  mulsprop  28122  lemulsd  28130  ltmuls1d  28165  ltmulnegs1d  28168  ltmulnegs2d  28169  lemuls1ad  28174  zsoring  28401  pw2gt0divsd  28437  pw2ge0divsd  28438  legso  28667  iscgra  28877  isleag  28915  iseqlg  28935  brbtwn2  28974  axlowdim  29030  ewlksfval  29670  isnvlem  30681  nvtri  30741  nmlnoubi  30867  nmblolbii  30870  nmblolbi  30871  blocnilem  30875  sii  30925  ubthlem2  30942  minvecolem3  30947  minvecolem5  30952  minvecolem6  30953  norm-ii  31209  norm3dif  31221  norm3adifi  31224  bcs  31252  pjnorm  31795  pjnel  31797  nmbdoplbi  32095  nmbdoplb  32096  nmcoplb  32101  lnconi  32104  nmbdfnlb  32121  nmcfnlb  32125  pjdifnormi  32238  mdslmd2i  32401  cvmd  32407  cvexch  32445  cdj1i  32504  cdj3lem1  32505  cdj3lem2b  32508  cdj3lem3b  32511  cdj3i  32512  fnfvor  32682  ofrco  32683  isoun  32775  nexple  32917  ismnt  33043  mgcmntco  33054  dfmgc2lem  33055  dfmgc2  33056  mgcf1o  33063  isinftm  33242  rlocaddval  33329  rlocmulval  33330  fldext2chn  33872  constrextdg2lem  33892  constrext2chn  33903  xrmulc1cn  34074  lmdvg  34097  faeval  34390  brfae  34392  inelcarsg  34455  carsgsigalem  34459  carsgclctunlem2  34463  carsgclctun  34465  hgt750lemc  34791  hgt750lemd  34792  hgt749d  34793  fineqvnttrclse  35268  sconnpht  35411  snmlval  35513  satfv1lem  35544  satfv1  35545  satfv0fun  35553  satfv0fvfmla0  35595  lediv2aALT  35859  faclim  35928  fvtransport  36214  idinside  36266  btwnconn1lem7  36275  btwnconn1lem11  36279  btwnconn1lem12  36280  ditgeq123dv  36403  cbvditgdavw2  36480  nn0prpwlem  36504  weiunval  36644  weiunfrlem  36646  bj-opabco  37502  poimirlem29  37970  heicant  37976  itg2addnclem  37992  itg2addnclem3  37994  itg2gt0cn  37996  ftc1anclem6  38019  ftc1anc  38022  ftc2nc  38023  dvasin  38025  areacirclem1  38029  seqpo  38068  incsequz  38069  metf1o  38076  mettrifi  38078  cntotbnd  38117  heiborlem4  38135  heiborlem6  38137  heiborlem10  38141  bfplem1  38143  bfplem2  38144  isopos  39626  oplecon3b  39646  atlatle  39766  4at2  40060  pmaple  40207  islaut  40529  lautcnvle  40535  lautco  40543  ltrncnvel  40588  cdlemeg49lebilem  40985  cdlemg17h  41114  tendoset  41205  tendotp  41207  cdlemk39s  41385  lcmineqlem23  42490  lcmineqlem  42491  intlewftc  42500  aks4d1p1p4  42510  dvle2  42511  aks4d1p8d2  42524  aks4d1p9  42527  aks4d1  42528  2ap1caineq  42584  sticksstones1  42585  sticksstones2  42586  sticksstones3  42587  sticksstones8  42592  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones15  42600  aks6d1c7lem3  42621  unitscyglem1  42634  brif12  42666  dvdsexpnn0  42766  dvdsexpb  42767  reltsub1  42818  irrapxlem2  43251  irrapxlem4  43253  irrapxlem5  43254  irrapxlem6  43255  pellexlem3  43259  monotuz  43369  monotoddzzfi  43370  monotoddzz  43371  jm2.17a  43388  jm2.17b  43389  rmygeid  43392  rmydioph  43442  expdiophlem1  43449  expdiophlem2  43450  ttac  43464  fnwe2lem2  43479  relexp01min  44140  cvgdvgrat  44740  relpeq1  45371  monoords  45730  supxrgelem  45767  supxrge  45768  abslt2sqd  45790  ltmulneg  45821  ltdiv23neg  45823  monoordxrv  45909  monoordxr  45910  monoord2xrv  45911  monoord2xr  45912  evthiccabs  45926  sqrlearg  45983  climinf  46036  climinff  46041  limsupres  46133  climinf2  46135  climinf2mpt  46142  climinfmpt  46143  supcnvlimsup  46168  liminfval2  46196  liminfltlem  46232  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  iblspltprt  46401  itgspltprt  46407  stoweidlem3  46431  fourierdlem2  46537  fourierdlem3  46538  fourierdlem11  46546  fourierdlem12  46547  fourierdlem15  46550  fourierdlem34  46569  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem79  46613  fourierdlem83  46617  fourierdlem89  46623  fourierdlem91  46625  fourierdlem100  46634  fourierdlem107  46641  fourierdlem109  46643  fourierdlem112  46646  etransclem31  46693  etransclem32  46694  rrndistlt  46718  ioorrnopn  46733  ioorrnopnxrlem  46734  sge0less  46820  sge0le  46835  sge0split  46837  sge0lempt  46838  sge0iunmptlemre  46843  sge0isum  46855  sge0seq  46874  meaiuninclem  46908  meaiininclem  46914  meaiininc  46915  isome  46922  omeunile  46933  omeiunlempt  46948  carageniuncllem2  46950  0ome  46957  isomenndlem  46958  isomennd  46959  ovnssle  46989  ovnsubadd  47000  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmvval0  47015  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hoidmvle  47028  hoidifhspdmvle  47048  hspmbllem2  47055  hspmbl  47057  ovnsubadd2lem  47073  ovolval4lem2  47078  ovolval4  47079  ovolval5lem2  47081  vonioolem2  47109  vonioo  47110  vonicclem2  47112  vonicc  47113  smfid  47180  smflimlem3  47201  ormkglobd  47305  natglobalincr  47307  chnerlem1  47312  squeezedltsq  47318  2elfz2melfz  47766  smonoord  47825  iccpart  47876  iccpartimp  47877  iccpartres  47878  sqrtpwpw2p  48001  grlicsym  48489  grlictr  48491  ismgmALT  48699  iscmgmALT  48700  issgrpALT  48701  iscsgrpALT  48702  lindslinindsimp2lem5  48938  rrx2plordisom  49199  aacllem  50276