Theorem breq12d 4947

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1508   class class class wbr 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-rab 3099  df-v 3419  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-sn 4445  df-pr 4447  df-op 4451  df-br 4935

This theorem is referenced by:  breq123d  4948  3brtr3d  4965  3brtr4d  4966  sbcbr  4989  pocl  5337  csbcnvgALT  5609  cnvpo  5981  sbcfung  6217  isoeq1  6899  isocnv  6912  isotr  6918  caovordig  7175  caovordg  7177  caovord2d  7179  caovord  7181  ofrfval  7241  ofrval  7243  ofrfval2  7251  caofref  7259  fnwelem  7636  fundmeng  8387  xpsneng  8404  xpcomeng  8411  xpdom2g  8415  limensuc  8496  infensuc  8497  unxpdom  8526  pssnn  8537  dif1en  8552  unfilem3  8585  unfi  8586  domunfican  8592  fodomfi  8598  marypha1lem  8698  infsupprpr  8769  wemaplem1  8811  wemaplem2  8812  wemapwe  8960  dif1card  9236  infxpenlem  9239  pwsdompw  9430  infmap2  9444  sornom  9503  isfin5  9525  isfin6  9526  domtriomlem  9668  axdc2lem  9674  axdclem2  9746  pwcfsdom  9809  cfpwsdom  9810  alephom  9811  fpwwe2lem7  9862  fpwwe2lem9  9864  tskcard  10007  ordpipq  10168  adderpqlem  10180  mulerpqlem  10181  mulcanenq  10186  lterpq  10196  ltanq  10197  ltmnq  10198  ltaddnq  10200  ltrnq  10205  archnq  10206  reclem4pr  10276  ltasr  10326  sqgt0sr  10332  axpre-ltadd  10393  axpre-mulgt0  10394  ltadd1  10914  leadd2  10916  ltmul2  11298  lemul2  11300  lemul1a  11301  ltdiv1  11311  ltdiv2  11333  lediv2  11337  div4p1lem1div2  11708  nn0ledivnn  12325  xleadd1  12470  xltadd2  12472  xsubge0  12476  xlemul1a  12503  xlemul1  12505  xlemul2  12506  xltmul2  12508  ltdifltdiv  13025  fzennn  13157  monoord  13221  monoord2  13222  expmordi  13352  ltexp2r  13358  leexp1a  13360  sqlecan  13392  bernneq  13411  faclbnd  13471  faclbnd3  13473  faclbnd4lem1  13474  faclbnd4lem2  13475  faclbnd4lem3  13476  faclbnd4lem4  13477  faclbnd6  13480  facubnd  13481  rlimcld2  14802  isercoll2  14892  climsup  14893  iseraltlem2  14906  fsumabs  15022  fsumrlim  15032  climcndslem1  15070  climcndslem2  15071  supcvg  15077  geomulcvg  15098  cvgrat  15105  ntrivcvgtail  15122  ruclem2  15451  ruclem8  15456  addmodlteqALT  15541  fproddvdsd  15550  sadcaddlem  15672  sadcadd  15673  nn0seqcvgd  15776  algcvg  15782  algcvga  15785  eucalgcvga  15792  isprm5  15913  qnumgt0  15952  pcprendvds2  16040  pcpremul  16042  pcadd2  16088  prmreclem4  16117  prmreclem5  16118  prmreclem6  16119  2expltfac  16288  xpsle  16722  mreexexlemd  16785  issubc  16975  latjlej2  17546  latmlem2  17562  sylow1lem3  18498  isslw  18506  fislw  18523  efgi  18615  lt6abl  18781  ablfac1eu  18957  isabv  19324  abvtri  19335  cayleyhamilton1  21219  isucn  22605  ispsmet  22632  psmettri2  22637  ismet  22651  isxmet  22652  xmettri2  22668  imasdsf1olem  22701  imasf1oxmet  22703  blvalps  22713  blval  22714  comet  22841  stdbdxmet  22843  nrmmetd  22902  tngngp  22981  tngngp3  22983  nmofval  23041  nmolb2d  23045  nmoi  23055  nmoix  23056  icopnfhmeo  23265  xrhmeo  23268  evth2  23282  pi1grplem  23371  minveclem6  23755  ovolfiniun  23820  ovoliunlem3  23823  voliunlem3  23871  ioombl1  23881  mbfmax  23968  mbfpos  23970  itg1climres  24033  mbfi1fseqlem2  24035  mbfi1fseqlem6  24039  mbfi1fseq  24040  mbfmullem  24044  itg2split  24068  itg2monolem1  24069  itg2monolem3  24071  itg2mono  24072  itg2i1fseqle  24073  itg2i1fseq  24074  itg2i1fseq2  24075  itg2addlem  24077  rolle  24305  dvlip  24308  c1lip1  24312  dvcnvrelem1  24332  dvcvx  24335  ply1divex  24448  q1pval  24465  fta1glem2  24478  fta1g  24479  fta1b  24481  plydivlem3  24602  fta1lem  24614  fta1  24615  aalioulem3  24641  aalioulem4  24642  aaliou3lem2  24650  aaliou3lem8  24652  aaliou3lem9  24657  ulmdvlem1  24706  ulmdvlem3  24708  abelthlem2  24738  abelthlem7a  24743  argrege0  24910  cxplt  24993  cxplea  24995  cxple2  24996  cxplt3  24999  logbleb  25077  logblt  25078  rlimcxp  25268  scvxcvx  25280  jensenlem2  25282  ftalem3  25369  ftalem7  25373  vmalelog  25498  chtub  25505  chpchtsum  25512  bclbnd  25573  efexple  25574  bposlem5  25581  bposlem6  25582  bposlem7  25583  lgsdilem  25617  2lgslem1a2  25683  2sqreuop  25755  2sqreuopnn  25756  2sqreuoplt  25757  2sqreuopltb  25758  2sqreuopnnlt  25759  2sqreuopnnltb  25760  dchrisumlem3  25784  dchrmusumlema  25786  dchrmusum2  25787  dchrvmasumlem2  25791  dchrvmasumlema  25793  dchrvmasumiflem1  25794  dchrisum0flblem2  25802  dchrisum0flb  25803  dchrisum0lema  25807  dchrisum0lem1b  25808  dchrisum0lem2  25811  pntrlog2bndlem2  25871  pntibndlem2  25884  pntlemf  25898  ostth2lem1  25911  qabvle  25918  legso  26102  iscgra  26312  isleag  26351  iseqlg  26371  brbtwn2  26409  axlowdim  26465  ewlksfval  27101  isnvlem  28179  nvtri  28239  nmlnoubi  28365  nmblolbii  28368  nmblolbi  28369  blocnilem  28373  sii  28423  ubthlem2  28441  minvecolem3  28446  minvecolem5  28451  minvecolem6  28452  norm-ii  28709  norm3dif  28721  norm3adifi  28724  bcs  28752  pjnorm  29297  pjnel  29299  nmbdoplbi  29597  nmbdoplb  29598  nmcoplb  29603  lnconi  29606  nmbdfnlb  29623  nmcfnlb  29627  pjdifnormi  29740  mdslmd2i  29903  cvmd  29909  cvexch  29947  cdj1i  30006  cdj3lem1  30007  cdj3lem2b  30010  cdj3lem3b  30013  cdj3i  30014  isoun  30213  isomnd  30446  omndadd  30451  omndmul  30459  ogrpinvlt  30469  isinftm  30508  gsumle  30554  xrmulc1cn  30849  lmdvg  30872  nexple  30944  faeval  31182  brfae  31184  inelcarsg  31246  carsgsigalem  31250  carsgclctunlem2  31254  carsgclctun  31256  hgt750lemc  31598  hgt750lemd  31599  hgt749d  31600  sconnpht  32101  snmlval  32203  lediv2aALT  32480  faclim  32538  poseq  32656  sltval2  32724  sltres  32730  nolesgn2o  32739  nodense  32757  nolt02o  32760  noresle  32761  nosupbnd2lem1  32776  nosupbnd2  32777  fvtransport  33054  idinside  33106  btwnconn1lem7  33115  btwnconn1lem11  33119  btwnconn1lem12  33120  nn0prpwlem  33231  poimirlem29  34402  heicant  34408  itg2addnclem  34424  itg2addnclem3  34426  itg2gt0cn  34428  ftc1anclem6  34453  ftc1anc  34456  ftc2nc  34457  dvasin  34459  areacirclem1  34463  seqpo  34504  incsequz  34505  metf1o  34512  mettrifi  34514  cntotbnd  34556  heiborlem4  34574  heiborlem6  34576  heiborlem10  34580  bfplem1  34582  bfplem2  34583  isopos  35801  oplecon3b  35821  atlatle  35941  4at2  36235  pmaple  36382  islaut  36704  lautcnvle  36710  lautco  36718  ltrncnvel  36763  cdlemeg49lebilem  37160  cdlemg17h  37289  tendoset  37380  tendotp  37382  cdlemk39s  37560  irrapxlem2  38857  irrapxlem4  38859  irrapxlem5  38860  irrapxlem6  38861  pellexlem3  38865  monotuz  38975  monotoddzzfi  38976  monotoddzz  38977  jm2.17a  38994  jm2.17b  38995  rmygeid  38998  rmydioph  39048  expdiophlem1  39055  expdiophlem2  39056  ttac  39070  fnwe2lem2  39088  relexp01min  39462  cvgdvgrat  40102  monoords  41028  supxrgelem  41069  supxrge  41070  abslt2sqd  41092  ltmulneg  41129  ltdiv23neg  41131  monoordxrv  41224  monoordxr  41225  monoord2xrv  41226  monoord2xr  41227  evthiccabs  41237  sqrlearg  41295  climinf  41353  climinff  41358  limsupres  41452  climinf2  41454  climinf2mpt  41461  climinfmpt  41462  supcnvlimsup  41487  liminfval2  41515  liminflelimsuplem  41522  liminfltlem  41551  fprodsubrecnncnvlem  41656  fprodaddrecnncnvlem  41658  ioodvbdlimc1lem1  41681  ioodvbdlimc1lem2  41682  ioodvbdlimc2lem  41684  iblspltprt  41723  itgspltprt  41729  stoweidlem3  41754  fourierdlem2  41860  fourierdlem3  41861  fourierdlem11  41869  fourierdlem12  41870  fourierdlem15  41873  fourierdlem34  41892  fourierdlem41  41899  fourierdlem48  41905  fourierdlem49  41906  fourierdlem79  41936  fourierdlem83  41940  fourierdlem89  41946  fourierdlem91  41948  fourierdlem100  41957  fourierdlem107  41964  fourierdlem109  41966  fourierdlem112  41969  etransclem31  42016  etransclem32  42017  rrndistlt  42041  ioorrnopn  42056  ioorrnopnxrlem  42057  sge0less  42140  sge0le  42155  sge0split  42157  sge0lempt  42158  sge0iunmptlemre  42163  sge0isum  42175  sge0seq  42194  meaiuninclem  42228  meaiininclem  42234  meaiininc  42235  isome  42242  omeunile  42253  omeiunlempt  42268  carageniuncllem2  42270  0ome  42277  isomenndlem  42278  isomennd  42279  ovnsslelem  42308  ovnssle  42309  ovnsubadd  42320  hsphoidmvle2  42333  hsphoidmvle  42334  hoidmvval0  42335  hoidmv1lelem1  42339  hoidmv1lelem2  42340  hoidmv1lelem3  42341  hoidmv1le  42342  hoidmvlelem1  42343  hoidmvlelem2  42344  hoidmvlelem3  42345  hoidmvlelem4  42346  hoidmvlelem5  42347  hoidmvle  42348  hoidifhspdmvle  42368  hspmbllem2  42375  hspmbl  42377  ovnsubadd2lem  42393  ovolval4lem2  42398  ovolval4  42399  ovolval5lem2  42401  vonioolem2  42429  vonioo  42430  vonicclem2  42432  vonicc  42433  smfid  42495  smflimlem3  42515  2elfz2melfz  42959  smonoord  42972  iccpart  42983  iccpartimp  42984  iccpartres  42985  sqrtpwpw2p  43103  ismgmALT  43529  iscmgmALT  43530  issgrpALT  43531  iscsgrpALT  43532  lindslinindsimp2lem5  43919  rrx2plordisom  44113  aacllem  44304