Theorem breq12d 5126

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  breq123d  5127  3brtr3d  5146  3brtr4d  5147  sbcbr  5170  pocl  5578  csbcnvgALTOLD  5875  cnvpo  6289  sbcfung  6561  isoeq1  7316  isocnv  7329  isotr  7335  caovordig  7616  caovordg  7618  caovord2d  7620  caovord  7622  ofrfvalg  7683  ofrval  7687  ofrfval2  7696  caofref  7706  fnwelem  8127  poseq  8154  fundmeng  9029  enrefnn  9043  xpsneng  9050  xpcomeng  9057  xpdom2g  9061  limensuc  9142  infensuc  9143  pssnn  9153  unxpdom  9219  dif1ennnALT  9237  unfilem3  9267  fodomfi  9272  domunfican  9281  marypha1lem  9393  infsupprpr  9466  wemaplem1  9508  wemaplem2  9509  wemapwe  9666  ssttrcl  9684  ttrcltr  9685  ttrclss  9689  dmttrcl  9690  rnttrcl  9691  ttrclselem2  9695  dif1card  9994  infxpenlem  9997  nnadju  10181  pwsdompw  10186  infmap2  10200  sornom  10261  isfin5  10283  isfin6  10284  domtriomlem  10426  axdc2lem  10432  axdclem2  10504  pwcfsdom  10568  cfpwsdom  10569  alephom  10570  fpwwe2lem6  10621  fpwwe2lem8  10623  tskcard  10766  ordpipq  10927  adderpqlem  10939  mulerpqlem  10940  mulcanenq  10945  lterpq  10955  ltanq  10956  ltmnq  10957  ltaddnq  10959  ltrnq  10964  archnq  10965  reclem4pr  11035  ltasr  11085  sqgt0sr  11091  axpre-ltadd  11152  axpre-mulgt0  11153  ltadd1  11681  leadd2  11683  ltmul2  12066  lemul2  12068  lemul1a  12069  ltdiv1  12079  ltdiv2  12101  lediv2  12105  div4p1lem1div2  12499  nn0ledivnn  13131  xleadd1  13281  xltadd2  13283  xsubge0  13287  xlemul1a  13314  xlemul1  13316  xlemul2  13317  xltmul2  13319  ltdifltdiv  13867  fzennn  14004  monoord  14068  monoord2  14069  expmordi  14203  ltexp2r  14209  leexp1a  14211  sqlecan  14245  bernneq  14265  faclbnd  14326  faclbnd3  14328  faclbnd4lem1  14329  faclbnd4lem2  14330  faclbnd4lem3  14331  faclbnd4lem4  14332  faclbnd6  14335  facubnd  14336  rlimcld2  15629  isercoll2  15720  climsup  15721  iseraltlem2  15734  fsumabs  15853  fsumrlim  15863  climcndslem1  15903  climcndslem2  15904  supcvg  15910  geomulcvg  15930  cvgrat  15937  ntrivcvgtail  15954  ruclem2  16288  ruclem8  16293  addmodlteqALT  16383  fproddvdsd  16393  sadcaddlem  16515  sadcadd  16516  nn0seqcvgd  16628  algcvg  16634  algcvga  16637  eucalgcvga  16644  isprm5  16766  qnumgt0  16809  pcprendvds2  16901  pcpremul  16903  pcadd2  16950  prmreclem4  16979  prmreclem5  16980  prmreclem6  16981  2expltfac  17152  xpsle  17633  mreexexlemd  17700  issubc  17892  latjlej2  18510  latmlem2  18526  ischn  18663  chnltm1  18665  chnind  18677  chnub  18678  sylow1lem3  19670  isslw  19678  fislw  19695  efgi  19789  lt6abl  19965  ablfac1eu  20145  isomnd  20193  omndadd  20198  omndmul  20205  ogrpinvlt  20214  gsumle  20215  isabv  20892  abvtri  20903  psdmul  22298  cayleyhamilton1  23018  isucn  24403  ispsmet  24430  psmettri2  24435  ismet  24449  isxmet  24450  xmettri2  24466  imasdsf1olem  24499  imasf1oxmet  24501  blvalps  24511  blval  24512  comet  24639  stdbdxmet  24641  nrmmetd  24700  tngngp  24780  tngngp3  24782  nmofval  24840  nmolb2d  24844  nmoi  24854  nmoix  24855  icopnfhmeo  25071  xrhmeo  25074  evth2  25088  pi1grplem  25177  minveclem6  25562  ovolfiniun  25629  ovoliunlem3  25632  voliunlem3  25680  ioombl1  25690  mbfmax  25777  mbfpos  25779  itg1climres  25842  mbfi1fseqlem2  25844  mbfi1fseqlem6  25848  mbfi1fseq  25849  mbfmullem  25853  itg2split  25877  itg2monolem1  25878  itg2monolem3  25880  itg2mono  25881  itg2i1fseqle  25882  itg2i1fseq  25883  itg2i1fseq2  25884  itg2addlem  25886  rolle  26118  dvlip  26121  c1lip1  26125  dvcnvrelem1  26145  dvcvx  26148  ply1divex  26263  q1pval  26281  fta1glem2  26295  fta1g  26296  fta1b  26298  plydivlem3  26425  fta1lem  26437  fta1  26438  aalioulem3  26464  aalioulem4  26465  aaliou3lem2  26473  aaliou3lem8  26475  aaliou3lem9  26480  ulmdvlem1  26529  ulmdvlem3  26531  abelthlem2  26561  abelthlem7a  26566  argrege0  26742  cxplt  26825  cxplea  26827  cxple2  26828  cxplt3  26831  logbleb  26914  logblt  26915  rlimcxp  27104  scvxcvx  27116  jensenlem2  27118  ftalem3  27205  ftalem7  27209  vmalelog  27335  chtub  27342  chpchtsum  27349  bclbnd  27410  efexple  27411  bposlem5  27418  bposlem6  27419  bposlem7  27420  lgsdilem  27454  2lgslem1a2  27520  2sqreuop  27592  2sqreuopnn  27593  2sqreuoplt  27594  2sqreuopltb  27595  2sqreuopnnlt  27596  2sqreuopnnltb  27597  dchrisumlem3  27621  dchrmusumlema  27623  dchrmusum2  27624  dchrvmasumlem2  27628  dchrvmasumlema  27630  dchrvmasumiflem1  27631  dchrisum0flblem2  27639  dchrisum0flb  27640  dchrisum0lema  27644  dchrisum0lem1b  27645  dchrisum0lem2  27648  pntrlog2bndlem2  27708  pntibndlem2  27721  pntlemf  27735  ostth2lem1  27748  qabvle  27755  ltsval2  27786  ltsres  27792  nolesgn2o  27801  nogesgn1o  27803  nodense  27822  nolt02o  27825  nogt01o  27826  noresle  27827  nosupbnd2lem1  27845  nosupbnd2  27846  noinfbnd2lem1  27860  noinfbnd2  27861  addsproplem1  28128  addsprop  28135  ltadds2im  28145  leadds2im  28147  leadds1  28148  leadds2  28149  ltadds1  28151  ltsubs1  28235  ltsubs2  28236  ltsubsubsbd  28242  ltsubsubs2bd  28243  posdifsd  28257  subsge0d  28259  mulsproplemcbv  28274  mulsproplem1  28275  mulsprop  28289  lemulsd  28297  ltmuls1d  28332  ltmulnegs1d  28335  ltmulnegs2d  28336  lemuls1ad  28341  zsoring  28568  pw2gt0divsd  28604  pw2ge0divsd  28605  legso  28834  iscgra  29077  isleag  29119  iseqlg  29139  brbtwn2  29196  axlowdim  29252  ewlksfval  29892  isnvlem  30903  nvtri  30963  nmlnoubi  31089  nmblolbii  31092  nmblolbi  31093  blocnilem  31097  sii  31147  ubthlem2  31164  minvecolem3  31169  minvecolem5  31174  minvecolem6  31175  norm-ii  31431  norm3dif  31443  norm3adifi  31446  bcs  31474  pjnorm  32017  pjnel  32019  nmbdoplbi  32317  nmbdoplb  32318  nmcoplb  32323  lnconi  32326  nmbdfnlb  32343  nmcfnlb  32347  pjdifnormi  32460  mdslmd2i  32623  cvmd  32629  cvexch  32667  cdj1i  32726  cdj3lem1  32727  cdj3lem2b  32730  cdj3lem3b  32733  cdj3i  32734  fnfvor  32895  ofrco  32896  isoun  32988  nexple  33118  ismnt  33244  mgcmntco  33255  dfmgc2lem  33256  dfmgc2  33257  mgcf1o  33264  isinftm  33442  rlocaddval  33530  rlocmulval  33531  fldext2chn  34063  constrextdg2lem  34083  constrext2chn  34094  xrmulc1cn  34265  lmdvg  34288  faeval  34581  brfae  34583  inelcarsg  34646  carsgsigalem  34650  carsgclctunlem2  34654  carsgclctun  34656  hgt750lemc  34979  hgt750lemd  34980  hgt749d  34981  fineqvnttrclse  35460  sconnpht  35620  snmlval  35722  satfv1lem  35753  satfv1  35754  satfv0fun  35762  satfv0fvfmla0  35804  lediv2aALT  36068  faclim  36137  fvtransport  36423  idinside  36475  btwnconn1lem7  36484  btwnconn1lem11  36488  btwnconn1lem12  36489  ditgeq123dv  36622  cbvditgdavw2  36699  nn0prpwlem  36722  weiunval  36862  weiunfrlem  36864  bj-opabco  37720  poimirlem29  38188  heicant  38194  itg2addnclem  38210  itg2addnclem3  38212  itg2gt0cn  38214  ftc1anclem6  38237  ftc1anc  38240  ftc2nc  38241  dvasin  38243  areacirclem1  38247  seqpo  38286  incsequz  38287  metf1o  38294  mettrifi  38296  cntotbnd  38335  heiborlem4  38353  heiborlem6  38355  heiborlem10  38359  bfplem1  38361  bfplem2  38362  isopos  39844  oplecon3b  39864  atlatle  39984  4at2  40278  pmaple  40425  islaut  40747  lautcnvle  40753  lautco  40761  ltrncnvel  40806  cdlemeg49lebilem  41203  cdlemg17h  41332  tendoset  41423  tendotp  41425  cdlemk39s  41603  lcmineqlem23  42708  lcmineqlem  42709  intlewftc  42718  aks4d1p1p4  42728  dvle2  42729  aks4d1p8d2  42742  aks4d1p9  42745  aks4d1  42746  2ap1caineq  42802  sticksstones1  42803  sticksstones2  42804  sticksstones3  42805  sticksstones8  42810  sticksstones10  42812  sticksstones11  42813  sticksstones12a  42814  sticksstones15  42818  aks6d1c7lem3  42839  unitscyglem1  42852  brif12  42886  dvdsexpnn0  42985  dvdsexpb  42986  reltsub1  43037  irrapxlem2  43442  irrapxlem4  43444  irrapxlem5  43445  irrapxlem6  43446  pellexlem3  43450  monotuz  43560  monotoddzzfi  43561  monotoddzz  43562  jm2.17a  43579  jm2.17b  43580  rmygeid  43583  rmydioph  43633  expdiophlem1  43640  expdiophlem2  43641  ttac  43655  fnwe2lem2  43670  relexp01min  44331  cvgdvgrat  44915  relpeq1  45545  monoords  45908  supxrgelem  45945  supxrge  45946  abslt2sqd  45968  ltmulneg  45999  ltdiv23neg  46001  monoordxrv  46087  monoordxr  46088  monoord2xrv  46089  monoord2xr  46090  evthiccabs  46104  sqrlearg  46161  climinf  46214  climinff  46219  limsupres  46311  climinf2  46313  climinf2mpt  46320  climinfmpt  46321  supcnvlimsup  46346  liminfval2  46374  liminfltlem  46410  fprodsubrecnncnvlem  46513  fprodaddrecnncnvlem  46515  ioodvbdlimc1lem1  46537  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  iblspltprt  46579  itgspltprt  46585  stoweidlem3  46609  fourierdlem2  46715  fourierdlem3  46716  fourierdlem11  46724  fourierdlem12  46725  fourierdlem15  46728  fourierdlem34  46747  fourierdlem41  46754  fourierdlem48  46760  fourierdlem49  46761  fourierdlem79  46791  fourierdlem83  46795  fourierdlem89  46801  fourierdlem91  46803  fourierdlem100  46812  fourierdlem107  46819  fourierdlem109  46821  fourierdlem112  46824  etransclem31  46871  etransclem32  46872  rrndistlt  46896  ioorrnopn  46911  ioorrnopnxrlem  46912  sge0less  46998  sge0le  47013  sge0split  47015  sge0lempt  47016  sge0iunmptlemre  47021  sge0isum  47033  sge0seq  47052  meaiuninclem  47086  meaiininclem  47092  meaiininc  47093  isome  47100  omeunile  47111  omeiunlempt  47126  carageniuncllem2  47128  0ome  47135  isomenndlem  47136  isomennd  47137  ovnssle  47167  ovnsubadd  47178  hsphoidmvle2  47191  hsphoidmvle  47192  hoidmvval0  47193  hoidmv1lelem1  47197  hoidmv1lelem2  47198  hoidmv1lelem3  47199  hoidmv1le  47200  hoidmvlelem1  47201  hoidmvlelem2  47202  hoidmvlelem3  47203  hoidmvlelem4  47204  hoidmvlelem5  47205  hoidmvle  47206  hoidifhspdmvle  47226  hspmbllem2  47233  hspmbl  47235  ovnsubadd2lem  47251  ovolval4lem2  47256  ovolval4  47257  ovolval5lem2  47259  vonioolem2  47287  vonioo  47288  vonicclem2  47290  vonicc  47291  smfid  47358  smflimlem3  47379  ormkglobd  47483  natglobalincr  47485  chnerlem1  47490  squeezedltsq  47496  2elfz2melfz  47944  smonoord  48003  iccpart  48054  iccpartimp  48055  iccpartres  48056  sqrtpwpw2p  48179  grlicsym  48667  grlictr  48669  ismgmALT  48877  iscmgmALT  48878  issgrpALT  48879  iscsgrpALT  48880  lindslinindsimp2lem5  49127  rrx2plordisom  49388  aacllem  50475