Theorem breq12d 5078

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   class class class wbr 5065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-br 5066

This theorem is referenced by:  breq123d  5079  3brtr3d  5096  3brtr4d  5097  sbcbr  5120  pocl  5480  csbcnvgALT  5754  cnvpo  6137  sbcfung  6378  isoeq1  7069  isocnv  7082  isotr  7088  caovordig  7352  caovordg  7354  caovord2d  7356  caovord  7358  ofrfval  7416  ofrval  7418  ofrfval2  7426  caofref  7434  fnwelem  7824  fundmeng  8583  xpsneng  8601  xpcomeng  8608  xpdom2g  8612  limensuc  8693  infensuc  8694  unxpdom  8724  pssnn  8735  dif1en  8750  unfilem3  8783  unfi  8784  domunfican  8790  fodomfi  8796  marypha1lem  8896  infsupprpr  8967  wemaplem1  9009  wemaplem2  9010  wemapwe  9159  dif1card  9435  infxpenlem  9438  pwsdompw  9625  infmap2  9639  sornom  9698  isfin5  9720  isfin6  9721  domtriomlem  9863  axdc2lem  9869  axdclem2  9941  pwcfsdom  10004  cfpwsdom  10005  alephom  10006  fpwwe2lem7  10057  fpwwe2lem9  10059  tskcard  10202  ordpipq  10363  adderpqlem  10375  mulerpqlem  10376  mulcanenq  10381  lterpq  10391  ltanq  10392  ltmnq  10393  ltaddnq  10395  ltrnq  10400  archnq  10401  reclem4pr  10471  ltasr  10521  sqgt0sr  10527  axpre-ltadd  10588  axpre-mulgt0  10589  ltadd1  11106  leadd2  11108  ltmul2  11490  lemul2  11492  lemul1a  11493  ltdiv1  11503  ltdiv2  11525  lediv2  11529  div4p1lem1div2  11891  nn0ledivnn  12501  xleadd1  12647  xltadd2  12649  xsubge0  12653  xlemul1a  12680  xlemul1  12682  xlemul2  12683  xltmul2  12685  ltdifltdiv  13203  fzennn  13335  monoord  13399  monoord2  13400  expmordi  13530  ltexp2r  13536  leexp1a  13538  sqlecan  13570  bernneq  13589  faclbnd  13649  faclbnd3  13651  faclbnd4lem1  13652  faclbnd4lem2  13653  faclbnd4lem3  13654  faclbnd4lem4  13655  faclbnd6  13658  facubnd  13659  rlimcld2  14934  isercoll2  15024  climsup  15025  iseraltlem2  15038  fsumabs  15155  fsumrlim  15165  climcndslem1  15203  climcndslem2  15204  supcvg  15210  geomulcvg  15231  cvgrat  15238  ntrivcvgtail  15255  ruclem2  15584  ruclem8  15589  addmodlteqALT  15674  fproddvdsd  15683  sadcaddlem  15805  sadcadd  15806  nn0seqcvgd  15913  algcvg  15919  algcvga  15922  eucalgcvga  15929  isprm5  16050  qnumgt0  16089  pcprendvds2  16177  pcpremul  16179  pcadd2  16225  prmreclem4  16254  prmreclem5  16255  prmreclem6  16256  2expltfac  16425  xpsle  16851  mreexexlemd  16914  issubc  17104  latjlej2  17675  latmlem2  17691  sylow1lem3  18724  isslw  18732  fislw  18749  efgi  18844  lt6abl  19014  ablfac1eu  19194  isabv  19589  abvtri  19600  cayleyhamilton1  21499  isucn  22886  ispsmet  22913  psmettri2  22918  ismet  22932  isxmet  22933  xmettri2  22949  imasdsf1olem  22982  imasf1oxmet  22984  blvalps  22994  blval  22995  comet  23122  stdbdxmet  23124  nrmmetd  23183  tngngp  23262  tngngp3  23264  nmofval  23322  nmolb2d  23326  nmoi  23336  nmoix  23337  icopnfhmeo  23546  xrhmeo  23549  evth2  23563  pi1grplem  23652  minveclem6  24036  ovolfiniun  24101  ovoliunlem3  24104  voliunlem3  24152  ioombl1  24162  mbfmax  24249  mbfpos  24251  itg1climres  24314  mbfi1fseqlem2  24316  mbfi1fseqlem6  24320  mbfi1fseq  24321  mbfmullem  24325  itg2split  24349  itg2monolem1  24350  itg2monolem3  24352  itg2mono  24353  itg2i1fseqle  24354  itg2i1fseq  24355  itg2i1fseq2  24356  itg2addlem  24358  rolle  24586  dvlip  24589  c1lip1  24593  dvcnvrelem1  24613  dvcvx  24616  ply1divex  24729  q1pval  24746  fta1glem2  24759  fta1g  24760  fta1b  24762  plydivlem3  24883  fta1lem  24895  fta1  24896  aalioulem3  24922  aalioulem4  24923  aaliou3lem2  24931  aaliou3lem8  24933  aaliou3lem9  24938  ulmdvlem1  24987  ulmdvlem3  24989  abelthlem2  25019  abelthlem7a  25024  argrege0  25193  cxplt  25276  cxplea  25278  cxple2  25279  cxplt3  25282  logbleb  25360  logblt  25361  rlimcxp  25550  scvxcvx  25562  jensenlem2  25564  ftalem3  25651  ftalem7  25655  vmalelog  25780  chtub  25787  chpchtsum  25794  bclbnd  25855  efexple  25856  bposlem5  25863  bposlem6  25864  bposlem7  25865  lgsdilem  25899  2lgslem1a2  25965  2sqreuop  26037  2sqreuopnn  26038  2sqreuoplt  26039  2sqreuopltb  26040  2sqreuopnnlt  26041  2sqreuopnnltb  26042  dchrisumlem3  26066  dchrmusumlema  26068  dchrmusum2  26069  dchrvmasumlem2  26073  dchrvmasumlema  26075  dchrvmasumiflem1  26076  dchrisum0flblem2  26084  dchrisum0flb  26085  dchrisum0lema  26089  dchrisum0lem1b  26090  dchrisum0lem2  26093  pntrlog2bndlem2  26153  pntibndlem2  26166  pntlemf  26180  ostth2lem1  26193  qabvle  26200  legso  26384  iscgra  26594  isleag  26632  iseqlg  26652  brbtwn2  26690  axlowdim  26746  ewlksfval  27382  isnvlem  28386  nvtri  28446  nmlnoubi  28572  nmblolbii  28575  nmblolbi  28576  blocnilem  28580  sii  28630  ubthlem2  28647  minvecolem3  28652  minvecolem5  28657  minvecolem6  28658  norm-ii  28914  norm3dif  28926  norm3adifi  28929  bcs  28957  pjnorm  29500  pjnel  29502  nmbdoplbi  29800  nmbdoplb  29801  nmcoplb  29806  lnconi  29809  nmbdfnlb  29826  nmcfnlb  29830  pjdifnormi  29943  mdslmd2i  30106  cvmd  30112  cvexch  30150  cdj1i  30209  cdj3lem1  30210  cdj3lem2b  30213  cdj3lem3b  30216  cdj3i  30217  isoun  30436  isomnd  30702  omndadd  30707  omndmul  30715  ogrpinvlt  30724  gsumle  30725  isinftm  30810  xrmulc1cn  31173  lmdvg  31196  nexple  31268  faeval  31505  brfae  31507  inelcarsg  31569  carsgsigalem  31573  carsgclctunlem2  31577  carsgclctun  31579  hgt750lemc  31918  hgt750lemd  31919  hgt749d  31920  sconnpht  32476  snmlval  32578  satfv1lem  32609  satfv1  32610  satfv0fun  32618  satfv0fvfmla0  32660  lediv2aALT  32920  faclim  32978  poseq  33095  sltval2  33163  sltres  33169  nolesgn2o  33178  nodense  33196  nolt02o  33199  noresle  33200  nosupbnd2lem1  33215  nosupbnd2  33216  fvtransport  33493  idinside  33545  btwnconn1lem7  33554  btwnconn1lem11  33558  btwnconn1lem12  33559  nn0prpwlem  33670  poimirlem29  34920  heicant  34926  itg2addnclem  34942  itg2addnclem3  34944  itg2gt0cn  34946  ftc1anclem6  34971  ftc1anc  34974  ftc2nc  34975  dvasin  34977  areacirclem1  34981  seqpo  35021  incsequz  35022  metf1o  35029  mettrifi  35031  cntotbnd  35073  heiborlem4  35091  heiborlem6  35093  heiborlem10  35097  bfplem1  35099  bfplem2  35100  isopos  36315  oplecon3b  36335  atlatle  36455  4at2  36749  pmaple  36896  islaut  37218  lautcnvle  37224  lautco  37232  ltrncnvel  37277  cdlemeg49lebilem  37674  cdlemg17h  37803  tendoset  37894  tendotp  37896  cdlemk39s  38074  reltsub1  39214  irrapxlem2  39418  irrapxlem4  39420  irrapxlem5  39421  irrapxlem6  39422  pellexlem3  39426  monotuz  39536  monotoddzzfi  39537  monotoddzz  39538  jm2.17a  39555  jm2.17b  39556  rmygeid  39559  rmydioph  39609  expdiophlem1  39616  expdiophlem2  39617  ttac  39631  fnwe2lem2  39649  relexp01min  40056  cvgdvgrat  40643  monoords  41562  supxrgelem  41603  supxrge  41604  abslt2sqd  41626  ltmulneg  41662  ltdiv23neg  41664  monoordxrv  41756  monoordxr  41757  monoord2xrv  41758  monoord2xr  41759  evthiccabs  41769  sqrlearg  41827  climinf  41885  climinff  41890  limsupres  41984  climinf2  41986  climinf2mpt  41993  climinfmpt  41994  supcnvlimsup  42019  liminfval2  42047  liminflelimsuplem  42054  liminfltlem  42083  fprodsubrecnncnvlem  42189  fprodaddrecnncnvlem  42191  ioodvbdlimc1lem1  42214  ioodvbdlimc1lem2  42215  ioodvbdlimc2lem  42217  iblspltprt  42256  itgspltprt  42262  stoweidlem3  42287  fourierdlem2  42393  fourierdlem3  42394  fourierdlem11  42402  fourierdlem12  42403  fourierdlem15  42406  fourierdlem34  42425  fourierdlem41  42432  fourierdlem48  42438  fourierdlem49  42439  fourierdlem79  42469  fourierdlem83  42473  fourierdlem89  42479  fourierdlem91  42481  fourierdlem100  42490  fourierdlem107  42497  fourierdlem109  42499  fourierdlem112  42502  etransclem31  42549  etransclem32  42550  rrndistlt  42574  ioorrnopn  42589  ioorrnopnxrlem  42590  sge0less  42673  sge0le  42688  sge0split  42690  sge0lempt  42691  sge0iunmptlemre  42696  sge0isum  42708  sge0seq  42727  meaiuninclem  42761  meaiininclem  42767  meaiininc  42768  isome  42775  omeunile  42786  omeiunlempt  42801  carageniuncllem2  42803  0ome  42810  isomenndlem  42811  isomennd  42812  ovnsslelem  42841  ovnssle  42842  ovnsubadd  42853  hsphoidmvle2  42866  hsphoidmvle  42867  hoidmvval0  42868  hoidmv1lelem1  42872  hoidmv1lelem2  42873  hoidmv1lelem3  42874  hoidmv1le  42875  hoidmvlelem1  42876  hoidmvlelem2  42877  hoidmvlelem3  42878  hoidmvlelem4  42879  hoidmvlelem5  42880  hoidmvle  42881  hoidifhspdmvle  42901  hspmbllem2  42908  hspmbl  42910  ovnsubadd2lem  42926  ovolval4lem2  42931  ovolval4  42932  ovolval5lem2  42934  vonioolem2  42962  vonioo  42963  vonicclem2  42965  vonicc  42966  smfid  43028  smflimlem3  43048  2elfz2melfz  43517  smonoord  43530  iccpart  43575  iccpartimp  43576  iccpartres  43577  sqrtpwpw2p  43699  ismgmALT  44129  iscmgmALT  44130  issgrpALT  44131  iscsgrpALT  44132  lindslinindsimp2lem5  44516  rrx2plordisom  44709  aacllem  44901