Theorem breq12d 5099

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

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

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  breq123d  5100  3brtr3d  5117  3brtr4d  5118  sbcbr  5141  pocl  5541  csbcnvgALT  5834  cnvpo  6246  sbcfung  6517  isoeq1  7266  isocnv  7279  isotr  7285  caovordig  7566  caovordg  7568  caovord2d  7570  caovord  7572  ofrfvalg  7633  ofrval  7637  ofrfval2  7646  caofref  7656  fnwelem  8075  poseq  8102  fundmeng  8973  enrefnn  8987  xpsneng  8994  xpcomeng  9001  xpdom2g  9005  limensuc  9086  infensuc  9087  pssnn  9097  unxpdom  9163  dif1ennnALT  9181  unfilem3  9211  fodomfi  9216  domunfican  9226  fodomfiOLD  9234  marypha1lem  9340  infsupprpr  9413  wemaplem1  9455  wemaplem2  9456  wemapwe  9612  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  dmttrcl  9636  rnttrcl  9637  ttrclselem2  9641  dif1card  9926  infxpenlem  9929  nnadju  10114  pwsdompw  10119  infmap2  10133  sornom  10193  isfin5  10215  isfin6  10216  domtriomlem  10358  axdc2lem  10364  axdclem2  10436  pwcfsdom  10500  cfpwsdom  10501  alephom  10502  fpwwe2lem6  10553  fpwwe2lem8  10555  tskcard  10698  ordpipq  10859  adderpqlem  10871  mulerpqlem  10872  mulcanenq  10877  lterpq  10887  ltanq  10888  ltmnq  10889  ltaddnq  10891  ltrnq  10896  archnq  10897  reclem4pr  10967  ltasr  11017  sqgt0sr  11023  axpre-ltadd  11084  axpre-mulgt0  11085  ltadd1  11611  leadd2  11613  ltmul2  12000  lemul2  12002  lemul1a  12003  ltdiv1  12014  ltdiv2  12036  lediv2  12040  div4p1lem1div2  12426  nn0ledivnn  13051  xleadd1  13201  xltadd2  13203  xsubge0  13207  xlemul1a  13234  xlemul1  13236  xlemul2  13237  xltmul2  13239  ltdifltdiv  13787  fzennn  13924  monoord  13988  monoord2  13989  expmordi  14123  ltexp2r  14129  leexp1a  14131  sqlecan  14165  bernneq  14185  faclbnd  14246  faclbnd3  14248  faclbnd4lem1  14249  faclbnd4lem2  14250  faclbnd4lem3  14251  faclbnd4lem4  14252  faclbnd6  14255  facubnd  14256  rlimcld2  15534  isercoll2  15625  climsup  15626  iseraltlem2  15639  fsumabs  15758  fsumrlim  15768  climcndslem1  15808  climcndslem2  15809  supcvg  15815  geomulcvg  15835  cvgrat  15842  ntrivcvgtail  15859  ruclem2  16193  ruclem8  16198  addmodlteqALT  16288  fproddvdsd  16298  sadcaddlem  16420  sadcadd  16421  nn0seqcvgd  16533  algcvg  16539  algcvga  16542  eucalgcvga  16549  isprm5  16671  qnumgt0  16714  pcprendvds2  16806  pcpremul  16808  pcadd2  16855  prmreclem4  16884  prmreclem5  16885  prmreclem6  16886  2expltfac  17057  xpsle  17537  mreexexlemd  17604  issubc  17796  latjlej2  18414  latmlem2  18430  ischn  18567  chnltm1  18569  chnind  18581  chnub  18582  sylow1lem3  19569  isslw  19577  fislw  19594  efgi  19688  lt6abl  19864  ablfac1eu  20044  isomnd  20092  omndadd  20097  omndmul  20104  ogrpinvlt  20113  gsumle  20114  isabv  20782  abvtri  20793  psdmul  22145  cayleyhamilton1  22870  isucn  24255  ispsmet  24282  psmettri2  24287  ismet  24301  isxmet  24302  xmettri2  24318  imasdsf1olem  24351  imasf1oxmet  24353  blvalps  24363  blval  24364  comet  24491  stdbdxmet  24493  nrmmetd  24552  tngngp  24632  tngngp3  24634  nmofval  24692  nmolb2d  24696  nmoi  24706  nmoix  24707  icopnfhmeo  24923  xrhmeo  24926  evth2  24940  pi1grplem  25029  minveclem6  25414  ovolfiniun  25481  ovoliunlem3  25484  voliunlem3  25532  ioombl1  25542  mbfmax  25629  mbfpos  25631  itg1climres  25694  mbfi1fseqlem2  25696  mbfi1fseqlem6  25700  mbfi1fseq  25701  mbfmullem  25705  itg2split  25729  itg2monolem1  25730  itg2monolem3  25732  itg2mono  25733  itg2i1fseqle  25734  itg2i1fseq  25735  itg2i1fseq2  25736  itg2addlem  25738  rolle  25970  dvlip  25973  c1lip1  25977  dvcnvrelem1  25997  dvcvx  26000  ply1divex  26115  q1pval  26133  fta1glem2  26147  fta1g  26148  fta1b  26150  plydivlem3  26275  fta1lem  26287  fta1  26288  aalioulem3  26314  aalioulem4  26315  aaliou3lem2  26323  aaliou3lem8  26325  aaliou3lem9  26330  ulmdvlem1  26381  ulmdvlem3  26383  abelthlem2  26413  abelthlem7a  26418  argrege0  26591  cxplt  26674  cxplea  26676  cxple2  26677  cxplt3  26680  logbleb  26763  logblt  26764  rlimcxp  26954  scvxcvx  26966  jensenlem2  26968  ftalem3  27055  ftalem7  27059  vmalelog  27185  chtub  27192  chpchtsum  27199  bclbnd  27260  efexple  27261  bposlem5  27268  bposlem6  27269  bposlem7  27270  lgsdilem  27304  2lgslem1a2  27370  2sqreuop  27442  2sqreuopnn  27443  2sqreuoplt  27444  2sqreuopltb  27445  2sqreuopnnlt  27446  2sqreuopnnltb  27447  dchrisumlem3  27471  dchrmusumlema  27473  dchrmusum2  27474  dchrvmasumlem2  27478  dchrvmasumlema  27480  dchrvmasumiflem1  27481  dchrisum0flblem2  27489  dchrisum0flb  27490  dchrisum0lema  27494  dchrisum0lem1b  27495  dchrisum0lem2  27498  pntrlog2bndlem2  27558  pntibndlem2  27571  pntlemf  27585  ostth2lem1  27598  qabvle  27605  ltsval2  27637  ltsres  27643  nolesgn2o  27652  nogesgn1o  27654  nodense  27673  nolt02o  27676  nogt01o  27677  noresle  27678  nosupbnd2lem1  27696  nosupbnd2  27697  noinfbnd2lem1  27711  noinfbnd2  27712  addsproplem1  27978  addsprop  27985  ltadds2im  27995  leadds2im  27997  leadds1  27998  leadds2  27999  ltadds1  28001  ltsubs1  28085  ltsubs2  28086  ltsubsubsbd  28092  ltsubsubs2bd  28093  posdifsd  28107  subsge0d  28109  mulsproplemcbv  28124  mulsproplem1  28125  mulsprop  28139  lemulsd  28147  ltmuls1d  28182  ltmulnegs1d  28185  ltmulnegs2d  28186  lemuls1ad  28191  zsoring  28418  pw2gt0divsd  28454  pw2ge0divsd  28455  legso  28684  iscgra  28894  isleag  28932  iseqlg  28952  brbtwn2  28991  axlowdim  29047  ewlksfval  29688  isnvlem  30699  nvtri  30759  nmlnoubi  30885  nmblolbii  30888  nmblolbi  30889  blocnilem  30893  sii  30943  ubthlem2  30960  minvecolem3  30965  minvecolem5  30970  minvecolem6  30971  norm-ii  31227  norm3dif  31239  norm3adifi  31242  bcs  31270  pjnorm  31813  pjnel  31815  nmbdoplbi  32113  nmbdoplb  32114  nmcoplb  32119  lnconi  32122  nmbdfnlb  32139  nmcfnlb  32143  pjdifnormi  32256  mdslmd2i  32419  cvmd  32425  cvexch  32463  cdj1i  32522  cdj3lem1  32523  cdj3lem2b  32526  cdj3lem3b  32529  cdj3i  32530  fnfvor  32700  ofrco  32701  isoun  32793  nexple  32935  ismnt  33061  mgcmntco  33072  dfmgc2lem  33073  dfmgc2  33074  mgcf1o  33081  isinftm  33260  rlocaddval  33347  rlocmulval  33348  fldext2chn  33891  constrextdg2lem  33911  constrext2chn  33922  xrmulc1cn  34093  lmdvg  34116  faeval  34409  brfae  34411  inelcarsg  34474  carsgsigalem  34478  carsgclctunlem2  34482  carsgclctun  34484  hgt750lemc  34810  hgt750lemd  34811  hgt749d  34812  fineqvnttrclse  35287  sconnpht  35430  snmlval  35532  satfv1lem  35563  satfv1  35564  satfv0fun  35572  satfv0fvfmla0  35614  lediv2aALT  35878  faclim  35947  fvtransport  36233  idinside  36285  btwnconn1lem7  36294  btwnconn1lem11  36298  btwnconn1lem12  36299  ditgeq123dv  36422  cbvditgdavw2  36499  nn0prpwlem  36523  weiunval  36663  weiunfrlem  36665  bj-opabco  37521  poimirlem29  37987  heicant  37993  itg2addnclem  38009  itg2addnclem3  38011  itg2gt0cn  38013  ftc1anclem6  38036  ftc1anc  38039  ftc2nc  38040  dvasin  38042  areacirclem1  38046  seqpo  38085  incsequz  38086  metf1o  38093  mettrifi  38095  cntotbnd  38134  heiborlem4  38152  heiborlem6  38154  heiborlem10  38158  bfplem1  38160  bfplem2  38161  isopos  39643  oplecon3b  39663  atlatle  39783  4at2  40077  pmaple  40224  islaut  40546  lautcnvle  40552  lautco  40560  ltrncnvel  40605  cdlemeg49lebilem  41002  cdlemg17h  41131  tendoset  41222  tendotp  41224  cdlemk39s  41402  lcmineqlem23  42507  lcmineqlem  42508  intlewftc  42517  aks4d1p1p4  42527  dvle2  42528  aks4d1p8d2  42541  aks4d1p9  42544  aks4d1  42545  2ap1caineq  42601  sticksstones1  42602  sticksstones2  42603  sticksstones3  42604  sticksstones8  42609  sticksstones10  42611  sticksstones11  42612  sticksstones12a  42613  sticksstones15  42617  aks6d1c7lem3  42638  unitscyglem1  42651  brif12  42683  dvdsexpnn0  42783  dvdsexpb  42784  reltsub1  42835  irrapxlem2  43272  irrapxlem4  43274  irrapxlem5  43275  irrapxlem6  43276  pellexlem3  43280  monotuz  43390  monotoddzzfi  43391  monotoddzz  43392  jm2.17a  43409  jm2.17b  43410  rmygeid  43413  rmydioph  43463  expdiophlem1  43470  expdiophlem2  43471  ttac  43485  fnwe2lem2  43500  relexp01min  44161  cvgdvgrat  44761  relpeq1  45392  monoords  45751  supxrgelem  45788  supxrge  45789  abslt2sqd  45811  ltmulneg  45842  ltdiv23neg  45844  monoordxrv  45930  monoordxr  45931  monoord2xrv  45932  monoord2xr  45933  evthiccabs  45947  sqrlearg  46004  climinf  46057  climinff  46062  limsupres  46154  climinf2  46156  climinf2mpt  46163  climinfmpt  46164  supcnvlimsup  46189  liminfval2  46217  liminfltlem  46253  fprodsubrecnncnvlem  46356  fprodaddrecnncnvlem  46358  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  iblspltprt  46422  itgspltprt  46428  stoweidlem3  46452  fourierdlem2  46558  fourierdlem3  46559  fourierdlem11  46567  fourierdlem12  46568  fourierdlem15  46571  fourierdlem34  46590  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  fourierdlem79  46634  fourierdlem83  46638  fourierdlem89  46644  fourierdlem91  46646  fourierdlem100  46655  fourierdlem107  46662  fourierdlem109  46664  fourierdlem112  46667  etransclem31  46714  etransclem32  46715  rrndistlt  46739  ioorrnopn  46754  ioorrnopnxrlem  46755  sge0less  46841  sge0le  46856  sge0split  46858  sge0lempt  46859  sge0iunmptlemre  46864  sge0isum  46876  sge0seq  46895  meaiuninclem  46929  meaiininclem  46935  meaiininc  46936  isome  46943  omeunile  46954  omeiunlempt  46969  carageniuncllem2  46971  0ome  46978  isomenndlem  46979  isomennd  46980  ovnssle  47010  ovnsubadd  47021  hsphoidmvle2  47034  hsphoidmvle  47035  hoidmvval0  47036  hoidmv1lelem1  47040  hoidmv1lelem2  47041  hoidmv1lelem3  47042  hoidmv1le  47043  hoidmvlelem1  47044  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvlelem4  47047  hoidmvlelem5  47048  hoidmvle  47049  hoidifhspdmvle  47069  hspmbllem2  47076  hspmbl  47078  ovnsubadd2lem  47094  ovolval4lem2  47099  ovolval4  47100  ovolval5lem2  47102  vonioolem2  47130  vonioo  47131  vonicclem2  47133  vonicc  47134  smfid  47201  smflimlem3  47222  ormkglobd  47324  natglobalincr  47326  chnerlem1  47331  squeezedltsq  47337  2elfz2melfz  47781  smonoord  47840  iccpart  47891  iccpartimp  47892  iccpartres  47893  sqrtpwpw2p  48016  grlicsym  48504  grlictr  48506  ismgmALT  48714  iscmgmALT  48715  issgrpALT  48716  iscsgrpALT  48717  lindslinindsimp2lem5  48953  rrx2plordisom  49214  aacllem  50291