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 585	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  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  5548  csbcnvgALT  5841  cnvpo  6253  sbcfung  6524  isoeq1  7273  isocnv  7286  isotr  7292  caovordig  7573  caovordg  7575  caovord2d  7577  caovord  7579  ofrfvalg  7640  ofrval  7644  ofrfval2  7653  caofref  7663  fnwelem  8083  poseq  8110  fundmeng  8981  enrefnn  8995  xpsneng  9002  xpcomeng  9009  xpdom2g  9013  limensuc  9094  infensuc  9095  pssnn  9105  unxpdom  9171  dif1ennnALT  9189  unfilem3  9219  fodomfi  9224  domunfican  9234  fodomfiOLD  9242  marypha1lem  9348  infsupprpr  9421  wemaplem1  9463  wemaplem2  9464  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  11616  leadd2  11618  ltmul2  12004  lemul2  12006  lemul1a  12007  ltdiv1  12018  ltdiv2  12040  lediv2  12044  div4p1lem1div2  12408  nn0ledivnn  13032  xleadd1  13182  xltadd2  13184  xsubge0  13188  xlemul1a  13215  xlemul1  13217  xlemul2  13218  xltmul2  13220  ltdifltdiv  13766  fzennn  13903  monoord  13967  monoord2  13968  expmordi  14102  ltexp2r  14108  leexp1a  14110  sqlecan  14144  bernneq  14164  faclbnd  14225  faclbnd3  14227  faclbnd4lem1  14228  faclbnd4lem2  14229  faclbnd4lem3  14230  faclbnd4lem4  14231  faclbnd6  14234  facubnd  14235  rlimcld2  15513  isercoll2  15604  climsup  15605  iseraltlem2  15618  fsumabs  15736  fsumrlim  15746  climcndslem1  15784  climcndslem2  15785  supcvg  15791  geomulcvg  15811  cvgrat  15818  ntrivcvgtail  15835  ruclem2  16169  ruclem8  16174  addmodlteqALT  16264  fproddvdsd  16274  sadcaddlem  16396  sadcadd  16397  nn0seqcvgd  16509  algcvg  16515  algcvga  16518  eucalgcvga  16525  isprm5  16646  qnumgt0  16689  pcprendvds2  16781  pcpremul  16783  pcadd2  16830  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  2expltfac  17032  xpsle  17512  mreexexlemd  17579  issubc  17771  latjlej2  18389  latmlem2  18405  ischn  18542  chnltm1  18544  chnind  18556  chnub  18557  sylow1lem3  19541  isslw  19549  fislw  19566  efgi  19660  lt6abl  19836  ablfac1eu  20016  isomnd  20064  omndadd  20069  omndmul  20076  ogrpinvlt  20085  gsumle  20086  isabv  20756  abvtri  20767  psdmul  22121  cayleyhamilton1  22848  isucn  24233  ispsmet  24260  psmettri2  24265  ismet  24279  isxmet  24280  xmettri2  24296  imasdsf1olem  24329  imasf1oxmet  24331  blvalps  24341  blval  24342  comet  24469  stdbdxmet  24471  nrmmetd  24530  tngngp  24610  tngngp3  24612  nmofval  24670  nmolb2d  24674  nmoi  24684  nmoix  24685  icopnfhmeo  24909  xrhmeo  24912  evth2  24927  pi1grplem  25017  minveclem6  25402  ovolfiniun  25470  ovoliunlem3  25473  voliunlem3  25521  ioombl1  25531  mbfmax  25618  mbfpos  25620  itg1climres  25683  mbfi1fseqlem2  25685  mbfi1fseqlem6  25689  mbfi1fseq  25690  mbfmullem  25694  itg2split  25718  itg2monolem1  25719  itg2monolem3  25721  itg2mono  25722  itg2i1fseqle  25723  itg2i1fseq  25724  itg2i1fseq2  25725  itg2addlem  25727  rolle  25962  dvlip  25966  c1lip1  25970  dvcnvrelem1  25990  dvcvx  25993  ply1divex  26110  q1pval  26128  fta1glem2  26142  fta1g  26143  fta1b  26145  plydivlem3  26271  fta1lem  26283  fta1  26284  aalioulem3  26310  aalioulem4  26311  aaliou3lem2  26319  aaliou3lem8  26321  aaliou3lem9  26326  ulmdvlem1  26377  ulmdvlem3  26379  abelthlem2  26410  abelthlem7a  26415  argrege0  26588  cxplt  26671  cxplea  26673  cxple2  26674  cxplt3  26677  logbleb  26761  logblt  26762  rlimcxp  26952  scvxcvx  26964  jensenlem2  26966  ftalem3  27053  ftalem7  27057  vmalelog  27184  chtub  27191  chpchtsum  27198  bclbnd  27259  efexple  27260  bposlem5  27267  bposlem6  27268  bposlem7  27269  lgsdilem  27303  2lgslem1a2  27369  2sqreuop  27441  2sqreuopnn  27442  2sqreuoplt  27443  2sqreuopltb  27444  2sqreuopnnlt  27445  2sqreuopnnltb  27446  dchrisumlem3  27470  dchrmusumlema  27472  dchrmusum2  27473  dchrvmasumlem2  27477  dchrvmasumlema  27479  dchrvmasumiflem1  27480  dchrisum0flblem2  27488  dchrisum0flb  27489  dchrisum0lema  27493  dchrisum0lem1b  27494  dchrisum0lem2  27497  pntrlog2bndlem2  27557  pntibndlem2  27570  pntlemf  27584  ostth2lem1  27597  qabvle  27604  ltsval2  27636  ltsres  27642  nolesgn2o  27651  nogesgn1o  27653  nodense  27672  nolt02o  27675  nogt01o  27676  noresle  27677  nosupbnd2lem1  27695  nosupbnd2  27696  noinfbnd2lem1  27710  noinfbnd2  27711  addsproplem1  27977  addsprop  27984  ltadds2im  27994  leadds2im  27996  leadds1  27997  leadds2  27998  ltadds1  28000  ltsubs1  28084  ltsubs2  28085  ltsubsubsbd  28091  ltsubsubs2bd  28092  posdifsd  28106  subsge0d  28108  mulsproplemcbv  28123  mulsproplem1  28124  mulsprop  28138  lemulsd  28146  ltmuls1d  28181  ltmulnegs1d  28184  ltmulnegs2d  28185  lemuls1ad  28190  zsoring  28417  pw2gt0divsd  28453  pw2ge0divsd  28454  legso  28683  iscgra  28893  isleag  28931  iseqlg  28951  brbtwn2  28990  axlowdim  29046  ewlksfval  29687  isnvlem  30698  nvtri  30758  nmlnoubi  30884  nmblolbii  30887  nmblolbi  30888  blocnilem  30892  sii  30942  ubthlem2  30959  minvecolem3  30964  minvecolem5  30969  minvecolem6  30970  norm-ii  31226  norm3dif  31238  norm3adifi  31241  bcs  31269  pjnorm  31812  pjnel  31814  nmbdoplbi  32112  nmbdoplb  32113  nmcoplb  32118  lnconi  32121  nmbdfnlb  32138  nmcfnlb  32142  pjdifnormi  32255  mdslmd2i  32418  cvmd  32424  cvexch  32462  cdj1i  32521  cdj3lem1  32522  cdj3lem2b  32525  cdj3lem3b  32528  cdj3i  32529  fnfvor  32699  ofrco  32700  isoun  32792  nexple  32936  ismnt  33076  mgcmntco  33087  dfmgc2lem  33088  dfmgc2  33089  mgcf1o  33096  isinftm  33275  rlocaddval  33362  rlocmulval  33363  fldext2chn  33906  constrextdg2lem  33926  constrext2chn  33937  xrmulc1cn  34108  lmdvg  34131  faeval  34424  brfae  34426  inelcarsg  34489  carsgsigalem  34493  carsgclctunlem2  34497  carsgclctun  34499  hgt750lemc  34825  hgt750lemd  34826  hgt749d  34827  fineqvnttrclse  35302  sconnpht  35445  snmlval  35547  satfv1lem  35578  satfv1  35579  satfv0fun  35587  satfv0fvfmla0  35629  lediv2aALT  35893  faclim  35962  fvtransport  36248  idinside  36300  btwnconn1lem7  36309  btwnconn1lem11  36313  btwnconn1lem12  36314  ditgeq123dv  36437  cbvditgdavw2  36514  nn0prpwlem  36538  weiunval  36678  weiunfrlem  36680  bj-opabco  37443  poimirlem29  37900  heicant  37906  itg2addnclem  37922  itg2addnclem3  37924  itg2gt0cn  37926  ftc1anclem6  37949  ftc1anc  37952  ftc2nc  37953  dvasin  37955  areacirclem1  37959  seqpo  37998  incsequz  37999  metf1o  38006  mettrifi  38008  cntotbnd  38047  heiborlem4  38065  heiborlem6  38067  heiborlem10  38071  bfplem1  38073  bfplem2  38074  isopos  39556  oplecon3b  39576  atlatle  39696  4at2  39990  pmaple  40137  islaut  40459  lautcnvle  40465  lautco  40473  ltrncnvel  40518  cdlemeg49lebilem  40915  cdlemg17h  41044  tendoset  41135  tendotp  41137  cdlemk39s  41315  lcmineqlem23  42421  lcmineqlem  42422  intlewftc  42431  aks4d1p1p4  42441  dvle2  42442  aks4d1p8d2  42455  aks4d1p9  42458  aks4d1  42459  2ap1caineq  42515  sticksstones1  42516  sticksstones2  42517  sticksstones3  42518  sticksstones8  42523  sticksstones10  42525  sticksstones11  42526  sticksstones12a  42527  sticksstones15  42531  aks6d1c7lem3  42552  unitscyglem1  42565  brif12  42597  dvdsexpnn0  42704  dvdsexpb  42705  reltsub1  42756  irrapxlem2  43180  irrapxlem4  43182  irrapxlem5  43183  irrapxlem6  43184  pellexlem3  43188  monotuz  43298  monotoddzzfi  43299  monotoddzz  43300  jm2.17a  43317  jm2.17b  43318  rmygeid  43321  rmydioph  43371  expdiophlem1  43378  expdiophlem2  43379  ttac  43393  fnwe2lem2  43408  relexp01min  44069  cvgdvgrat  44669  relpeq1  45300  monoords  45659  supxrgelem  45696  supxrge  45697  abslt2sqd  45719  ltmulneg  45750  ltdiv23neg  45752  monoordxrv  45839  monoordxr  45840  monoord2xrv  45841  monoord2xr  45842  evthiccabs  45856  sqrlearg  45913  climinf  45966  climinff  45971  limsupres  46063  climinf2  46065  climinf2mpt  46072  climinfmpt  46073  supcnvlimsup  46098  liminfval2  46126  liminfltlem  46162  fprodsubrecnncnvlem  46265  fprodaddrecnncnvlem  46267  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  iblspltprt  46331  itgspltprt  46337  stoweidlem3  46361  fourierdlem2  46467  fourierdlem3  46468  fourierdlem11  46476  fourierdlem12  46477  fourierdlem15  46480  fourierdlem34  46499  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  fourierdlem79  46543  fourierdlem83  46547  fourierdlem89  46553  fourierdlem91  46555  fourierdlem100  46564  fourierdlem107  46571  fourierdlem109  46573  fourierdlem112  46576  etransclem31  46623  etransclem32  46624  rrndistlt  46648  ioorrnopn  46663  ioorrnopnxrlem  46664  sge0less  46750  sge0le  46765  sge0split  46767  sge0lempt  46768  sge0iunmptlemre  46773  sge0isum  46785  sge0seq  46804  meaiuninclem  46838  meaiininclem  46844  meaiininc  46845  isome  46852  omeunile  46863  omeiunlempt  46878  carageniuncllem2  46880  0ome  46887  isomenndlem  46888  isomennd  46889  ovnssle  46919  ovnsubadd  46930  hsphoidmvle2  46943  hsphoidmvle  46944  hoidmvval0  46945  hoidmv1lelem1  46949  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmv1le  46952  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem4  46956  hoidmvlelem5  46957  hoidmvle  46958  hoidifhspdmvle  46978  hspmbllem2  46985  hspmbl  46987  ovnsubadd2lem  47003  ovolval4lem2  47008  ovolval4  47009  ovolval5lem2  47011  vonioolem2  47039  vonioo  47040  vonicclem2  47042  vonicc  47043  smfid  47110  smflimlem3  47131  ormkglobd  47233  natglobalincr  47235  chnerlem1  47240  squeezedltsq  47246  2elfz2melfz  47678  smonoord  47731  iccpart  47776  iccpartimp  47777  iccpartres  47778  sqrtpwpw2p  47898  grlicsym  48373  grlictr  48375  ismgmALT  48583  iscmgmALT  48584  issgrpALT  48585  iscsgrpALT  48586  lindslinindsimp2lem5  48822  rrx2plordisom  49083  aacllem  50160