Theorem breq12d 5113

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  breq123d  5114  3brtr3d  5131  3brtr4d  5132  sbcbr  5155  pocl  5563  csbcnvgALTOLD  5860  cnvpo  6274  sbcfung  6545  isoeq1  7301  isocnv  7314  isotr  7320  caovordig  7601  caovordg  7603  caovord2d  7605  caovord  7607  ofrfvalg  7668  ofrval  7672  ofrfval2  7681  caofref  7691  fnwelem  8111  poseq  8138  fundmeng  9013  enrefnn  9027  xpsneng  9034  xpcomeng  9041  xpdom2g  9045  limensuc  9126  infensuc  9127  pssnn  9137  unxpdom  9203  dif1ennnALT  9221  unfilem3  9251  fodomfi  9256  domunfican  9266  marypha1lem  9379  infsupprpr  9452  wemaplem1  9494  wemaplem2  9495  wemapwe  9652  ssttrcl  9670  ttrcltr  9671  ttrclss  9675  dmttrcl  9676  rnttrcl  9677  ttrclselem2  9681  dif1card  9966  infxpenlem  9969  nnadju  10154  pwsdompw  10159  infmap2  10173  sornom  10234  isfin5  10256  isfin6  10257  domtriomlem  10399  axdc2lem  10405  axdclem2  10477  pwcfsdom  10541  cfpwsdom  10542  alephom  10543  fpwwe2lem6  10594  fpwwe2lem8  10596  tskcard  10739  ordpipq  10900  adderpqlem  10912  mulerpqlem  10913  mulcanenq  10918  lterpq  10928  ltanq  10929  ltmnq  10930  ltaddnq  10932  ltrnq  10937  archnq  10938  reclem4pr  11008  ltasr  11058  sqgt0sr  11064  axpre-ltadd  11125  axpre-mulgt0  11126  ltadd1  11654  leadd2  11656  ltmul2  12042  lemul2  12044  lemul1a  12045  ltdiv1  12056  ltdiv2  12078  lediv2  12082  div4p1lem1div2  12476  nn0ledivnn  13108  xleadd1  13258  xltadd2  13260  xsubge0  13264  xlemul1a  13291  xlemul1  13293  xlemul2  13294  xltmul2  13296  ltdifltdiv  13844  fzennn  13981  monoord  14045  monoord2  14046  expmordi  14180  ltexp2r  14186  leexp1a  14188  sqlecan  14222  bernneq  14242  faclbnd  14303  faclbnd3  14305  faclbnd4lem1  14306  faclbnd4lem2  14307  faclbnd4lem3  14308  faclbnd4lem4  14309  faclbnd6  14312  facubnd  14313  rlimcld2  15605  isercoll2  15696  climsup  15697  iseraltlem2  15710  fsumabs  15829  fsumrlim  15839  climcndslem1  15879  climcndslem2  15880  supcvg  15886  geomulcvg  15906  cvgrat  15913  ntrivcvgtail  15930  ruclem2  16264  ruclem8  16269  addmodlteqALT  16359  fproddvdsd  16369  sadcaddlem  16491  sadcadd  16492  nn0seqcvgd  16604  algcvg  16610  algcvga  16613  eucalgcvga  16620  isprm5  16742  qnumgt0  16785  pcprendvds2  16877  pcpremul  16879  pcadd2  16926  prmreclem4  16955  prmreclem5  16956  prmreclem6  16957  2expltfac  17128  xpsle  17609  mreexexlemd  17676  issubc  17868  latjlej2  18486  latmlem2  18502  ischn  18639  chnltm1  18641  chnind  18653  chnub  18654  sylow1lem3  19640  isslw  19648  fislw  19665  efgi  19759  lt6abl  19935  ablfac1eu  20115  isomnd  20163  omndadd  20168  omndmul  20175  ogrpinvlt  20184  gsumle  20185  isabv  20860  abvtri  20871  psdmul  22231  cayleyhamilton1  22952  isucn  24337  ispsmet  24364  psmettri2  24369  ismet  24383  isxmet  24384  xmettri2  24400  imasdsf1olem  24433  imasf1oxmet  24435  blvalps  24445  blval  24446  comet  24573  stdbdxmet  24575  nrmmetd  24634  tngngp  24714  tngngp3  24716  nmofval  24774  nmolb2d  24778  nmoi  24788  nmoix  24789  icopnfhmeo  25005  xrhmeo  25008  evth2  25022  pi1grplem  25111  minveclem6  25496  ovolfiniun  25563  ovoliunlem3  25566  voliunlem3  25614  ioombl1  25624  mbfmax  25711  mbfpos  25713  itg1climres  25776  mbfi1fseqlem2  25778  mbfi1fseqlem6  25782  mbfi1fseq  25783  mbfmullem  25787  itg2split  25811  itg2monolem1  25812  itg2monolem3  25814  itg2mono  25815  itg2i1fseqle  25816  itg2i1fseq  25817  itg2i1fseq2  25818  itg2addlem  25820  rolle  26052  dvlip  26055  c1lip1  26059  dvcnvrelem1  26079  dvcvx  26082  ply1divex  26197  q1pval  26215  fta1glem2  26229  fta1g  26230  fta1b  26232  plydivlem3  26359  fta1lem  26371  fta1  26372  aalioulem3  26398  aalioulem4  26399  aaliou3lem2  26407  aaliou3lem8  26409  aaliou3lem9  26414  ulmdvlem1  26463  ulmdvlem3  26465  abelthlem2  26495  abelthlem7a  26500  argrege0  26676  cxplt  26759  cxplea  26761  cxple2  26762  cxplt3  26765  logbleb  26848  logblt  26849  rlimcxp  27038  scvxcvx  27050  jensenlem2  27052  ftalem3  27139  ftalem7  27143  vmalelog  27269  chtub  27276  chpchtsum  27283  bclbnd  27344  efexple  27345  bposlem5  27352  bposlem6  27353  bposlem7  27354  lgsdilem  27388  2lgslem1a2  27454  2sqreuop  27526  2sqreuopnn  27527  2sqreuoplt  27528  2sqreuopltb  27529  2sqreuopnnlt  27530  2sqreuopnnltb  27531  dchrisumlem3  27555  dchrmusumlema  27557  dchrmusum2  27558  dchrvmasumlem2  27562  dchrvmasumlema  27564  dchrvmasumiflem1  27565  dchrisum0flblem2  27573  dchrisum0flb  27574  dchrisum0lema  27578  dchrisum0lem1b  27579  dchrisum0lem2  27582  pntrlog2bndlem2  27642  pntibndlem2  27655  pntlemf  27669  ostth2lem1  27682  qabvle  27689  ltsval2  27720  ltsres  27726  nolesgn2o  27735  nogesgn1o  27737  nodense  27756  nolt02o  27759  nogt01o  27760  noresle  27761  nosupbnd2lem1  27779  nosupbnd2  27780  noinfbnd2lem1  27794  noinfbnd2  27795  addsproplem1  28062  addsprop  28069  ltadds2im  28079  leadds2im  28081  leadds1  28082  leadds2  28083  ltadds1  28085  ltsubs1  28169  ltsubs2  28170  ltsubsubsbd  28176  ltsubsubs2bd  28177  posdifsd  28191  subsge0d  28193  mulsproplemcbv  28208  mulsproplem1  28209  mulsprop  28223  lemulsd  28231  ltmuls1d  28266  ltmulnegs1d  28269  ltmulnegs2d  28270  lemuls1ad  28275  zsoring  28502  pw2gt0divsd  28538  pw2ge0divsd  28539  legso  28768  iscgra  29003  isleag  29041  iseqlg  29061  brbtwn2  29106  axlowdim  29162  ewlksfval  29802  isnvlem  30813  nvtri  30873  nmlnoubi  30999  nmblolbii  31002  nmblolbi  31003  blocnilem  31007  sii  31057  ubthlem2  31074  minvecolem3  31079  minvecolem5  31084  minvecolem6  31085  norm-ii  31341  norm3dif  31353  norm3adifi  31356  bcs  31384  pjnorm  31927  pjnel  31929  nmbdoplbi  32227  nmbdoplb  32228  nmcoplb  32233  lnconi  32236  nmbdfnlb  32253  nmcfnlb  32257  pjdifnormi  32370  mdslmd2i  32533  cvmd  32539  cvexch  32577  cdj1i  32636  cdj3lem1  32637  cdj3lem2b  32640  cdj3lem3b  32643  cdj3i  32644  fnfvor  32811  ofrco  32812  isoun  32904  nexple  33035  ismnt  33161  mgcmntco  33172  dfmgc2lem  33173  dfmgc2  33174  mgcf1o  33181  isinftm  33361  rlocaddval  33450  rlocmulval  33451  fldext2chn  34025  constrextdg2lem  34045  constrext2chn  34056  xrmulc1cn  34227  lmdvg  34250  faeval  34543  brfae  34545  inelcarsg  34608  carsgsigalem  34612  carsgclctunlem2  34616  carsgclctun  34618  hgt750lemc  34941  hgt750lemd  34942  hgt749d  34943  fineqvnttrclse  35420  sconnpht  35579  snmlval  35681  satfv1lem  35712  satfv1  35713  satfv0fun  35721  satfv0fvfmla0  35763  lediv2aALT  36027  faclim  36096  fvtransport  36382  idinside  36434  btwnconn1lem7  36443  btwnconn1lem11  36447  btwnconn1lem12  36448  ditgeq123dv  36581  cbvditgdavw2  36658  nn0prpwlem  36682  weiunval  36822  weiunfrlem  36824  bj-opabco  37680  poimirlem29  38148  heicant  38154  itg2addnclem  38170  itg2addnclem3  38172  itg2gt0cn  38174  ftc1anclem6  38197  ftc1anc  38200  ftc2nc  38201  dvasin  38203  areacirclem1  38207  seqpo  38246  incsequz  38247  metf1o  38254  mettrifi  38256  cntotbnd  38295  heiborlem4  38313  heiborlem6  38315  heiborlem10  38319  bfplem1  38321  bfplem2  38322  isopos  39804  oplecon3b  39824  atlatle  39944  4at2  40238  pmaple  40385  islaut  40707  lautcnvle  40713  lautco  40721  ltrncnvel  40766  cdlemeg49lebilem  41163  cdlemg17h  41292  tendoset  41383  tendotp  41385  cdlemk39s  41563  lcmineqlem23  42668  lcmineqlem  42669  intlewftc  42678  aks4d1p1p4  42688  dvle2  42689  aks4d1p8d2  42702  aks4d1p9  42705  aks4d1  42706  2ap1caineq  42762  sticksstones1  42763  sticksstones2  42764  sticksstones3  42765  sticksstones8  42770  sticksstones10  42772  sticksstones11  42773  sticksstones12a  42774  sticksstones15  42778  aks6d1c7lem3  42799  unitscyglem1  42812  brif12  42844  dvdsexpnn0  42943  dvdsexpb  42944  reltsub1  42995  irrapxlem2  43400  irrapxlem4  43402  irrapxlem5  43403  irrapxlem6  43404  pellexlem3  43408  monotuz  43518  monotoddzzfi  43519  monotoddzz  43520  jm2.17a  43537  jm2.17b  43538  rmygeid  43541  rmydioph  43591  expdiophlem1  43598  expdiophlem2  43599  ttac  43613  fnwe2lem2  43628  relexp01min  44289  cvgdvgrat  44889  relpeq1  45520  monoords  45876  supxrgelem  45913  supxrge  45914  abslt2sqd  45936  ltmulneg  45967  ltdiv23neg  45969  monoordxrv  46055  monoordxr  46056  monoord2xrv  46057  monoord2xr  46058  evthiccabs  46072  sqrlearg  46129  climinf  46182  climinff  46187  limsupres  46279  climinf2  46281  climinf2mpt  46288  climinfmpt  46289  supcnvlimsup  46314  liminfval2  46342  liminfltlem  46378  fprodsubrecnncnvlem  46481  fprodaddrecnncnvlem  46483  ioodvbdlimc1lem1  46505  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  iblspltprt  46547  itgspltprt  46553  stoweidlem3  46577  fourierdlem2  46683  fourierdlem3  46684  fourierdlem11  46692  fourierdlem12  46693  fourierdlem15  46696  fourierdlem34  46715  fourierdlem41  46722  fourierdlem48  46728  fourierdlem49  46729  fourierdlem79  46759  fourierdlem83  46763  fourierdlem89  46769  fourierdlem91  46771  fourierdlem100  46780  fourierdlem107  46787  fourierdlem109  46789  fourierdlem112  46792  etransclem31  46839  etransclem32  46840  rrndistlt  46864  ioorrnopn  46879  ioorrnopnxrlem  46880  sge0less  46966  sge0le  46981  sge0split  46983  sge0lempt  46984  sge0iunmptlemre  46989  sge0isum  47001  sge0seq  47020  meaiuninclem  47054  meaiininclem  47060  meaiininc  47061  isome  47068  omeunile  47079  omeiunlempt  47094  carageniuncllem2  47096  0ome  47103  isomenndlem  47104  isomennd  47105  ovnssle  47135  ovnsubadd  47146  hsphoidmvle2  47159  hsphoidmvle  47160  hoidmvval0  47161  hoidmv1lelem1  47165  hoidmv1lelem2  47166  hoidmv1lelem3  47167  hoidmv1le  47168  hoidmvlelem1  47169  hoidmvlelem2  47170  hoidmvlelem3  47171  hoidmvlelem4  47172  hoidmvlelem5  47173  hoidmvle  47174  hoidifhspdmvle  47194  hspmbllem2  47201  hspmbl  47203  ovnsubadd2lem  47219  ovolval4lem2  47224  ovolval4  47225  ovolval5lem2  47227  vonioolem2  47255  vonioo  47256  vonicclem2  47258  vonicc  47259  smfid  47326  smflimlem3  47347  ormkglobd  47451  natglobalincr  47453  chnerlem1  47458  squeezedltsq  47464  2elfz2melfz  47912  smonoord  47971  iccpart  48022  iccpartimp  48023  iccpartres  48024  sqrtpwpw2p  48147  grlicsym  48635  grlictr  48637  ismgmALT  48845  iscmgmALT  48846  issgrpALT  48847  iscsgrpALT  48848  lindslinindsimp2lem5  49084  rrx2plordisom  49345  aacllem  50422