Theorem breq12d 5105

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   class class class wbr 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  breq123d  5106  3brtr3d  5123  3brtr4d  5124  sbcbr  5147  pocl  5535  csbcnvgALT  5827  cnvpo  6235  sbcfung  6506  isoeq1  7254  isocnv  7267  isotr  7273  caovordig  7554  caovordg  7556  caovord2d  7558  caovord  7560  ofrfvalg  7621  ofrval  7625  ofrfval2  7634  caofref  7644  fnwelem  8064  poseq  8091  fundmeng  8957  enrefnn  8972  xpsneng  8979  xpcomeng  8986  xpdom2g  8990  limensuc  9071  infensuc  9072  pssnn  9082  unxpdom  9148  dif1ennnALT  9166  unfilem3  9196  fodomfi  9201  domunfican  9211  fodomfiOLD  9220  marypha1lem  9323  infsupprpr  9396  wemaplem1  9438  wemaplem2  9439  wemapwe  9593  ssttrcl  9611  ttrcltr  9612  ttrclss  9616  dmttrcl  9617  rnttrcl  9618  ttrclselem2  9622  dif1card  9904  infxpenlem  9907  nnadju  10092  pwsdompw  10097  infmap2  10111  sornom  10171  isfin5  10193  isfin6  10194  domtriomlem  10336  axdc2lem  10342  axdclem2  10414  pwcfsdom  10477  cfpwsdom  10478  alephom  10479  fpwwe2lem6  10530  fpwwe2lem8  10532  tskcard  10675  ordpipq  10836  adderpqlem  10848  mulerpqlem  10849  mulcanenq  10854  lterpq  10864  ltanq  10865  ltmnq  10866  ltaddnq  10868  ltrnq  10873  archnq  10874  reclem4pr  10944  ltasr  10994  sqgt0sr  11000  axpre-ltadd  11061  axpre-mulgt0  11062  ltadd1  11587  leadd2  11589  ltmul2  11975  lemul2  11977  lemul1a  11978  ltdiv1  11989  ltdiv2  12011  lediv2  12015  div4p1lem1div2  12379  nn0ledivnn  13008  xleadd1  13157  xltadd2  13159  xsubge0  13163  xlemul1a  13190  xlemul1  13192  xlemul2  13193  xltmul2  13195  ltdifltdiv  13738  fzennn  13875  monoord  13939  monoord2  13940  expmordi  14074  ltexp2r  14080  leexp1a  14082  sqlecan  14116  bernneq  14136  faclbnd  14197  faclbnd3  14199  faclbnd4lem1  14200  faclbnd4lem2  14201  faclbnd4lem3  14202  faclbnd4lem4  14203  faclbnd6  14206  facubnd  14207  rlimcld2  15485  isercoll2  15576  climsup  15577  iseraltlem2  15590  fsumabs  15708  fsumrlim  15718  climcndslem1  15756  climcndslem2  15757  supcvg  15763  geomulcvg  15783  cvgrat  15790  ntrivcvgtail  15807  ruclem2  16141  ruclem8  16146  addmodlteqALT  16236  fproddvdsd  16246  sadcaddlem  16368  sadcadd  16369  nn0seqcvgd  16481  algcvg  16487  algcvga  16490  eucalgcvga  16497  isprm5  16618  qnumgt0  16661  pcprendvds2  16753  pcpremul  16755  pcadd2  16802  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  2expltfac  17004  xpsle  17483  mreexexlemd  17550  issubc  17742  latjlej2  18360  latmlem2  18376  sylow1lem3  19479  isslw  19487  fislw  19504  efgi  19598  lt6abl  19774  ablfac1eu  19954  isomnd  20002  omndadd  20007  omndmul  20014  ogrpinvlt  20023  gsumle  20024  isabv  20696  abvtri  20707  psdmul  22051  cayleyhamilton1  22777  isucn  24163  ispsmet  24190  psmettri2  24195  ismet  24209  isxmet  24210  xmettri2  24226  imasdsf1olem  24259  imasf1oxmet  24261  blvalps  24271  blval  24272  comet  24399  stdbdxmet  24401  nrmmetd  24460  tngngp  24540  tngngp3  24542  nmofval  24600  nmolb2d  24604  nmoi  24614  nmoix  24615  icopnfhmeo  24839  xrhmeo  24842  evth2  24857  pi1grplem  24947  minveclem6  25332  ovolfiniun  25400  ovoliunlem3  25403  voliunlem3  25451  ioombl1  25461  mbfmax  25548  mbfpos  25550  itg1climres  25613  mbfi1fseqlem2  25615  mbfi1fseqlem6  25619  mbfi1fseq  25620  mbfmullem  25624  itg2split  25648  itg2monolem1  25649  itg2monolem3  25651  itg2mono  25652  itg2i1fseqle  25653  itg2i1fseq  25654  itg2i1fseq2  25655  itg2addlem  25657  rolle  25892  dvlip  25896  c1lip1  25900  dvcnvrelem1  25920  dvcvx  25923  ply1divex  26040  q1pval  26058  fta1glem2  26072  fta1g  26073  fta1b  26075  plydivlem3  26201  fta1lem  26213  fta1  26214  aalioulem3  26240  aalioulem4  26241  aaliou3lem2  26249  aaliou3lem8  26251  aaliou3lem9  26256  ulmdvlem1  26307  ulmdvlem3  26309  abelthlem2  26340  abelthlem7a  26345  argrege0  26518  cxplt  26601  cxplea  26603  cxple2  26604  cxplt3  26607  logbleb  26691  logblt  26692  rlimcxp  26882  scvxcvx  26894  jensenlem2  26896  ftalem3  26983  ftalem7  26987  vmalelog  27114  chtub  27121  chpchtsum  27128  bclbnd  27189  efexple  27190  bposlem5  27197  bposlem6  27198  bposlem7  27199  lgsdilem  27233  2lgslem1a2  27299  2sqreuop  27371  2sqreuopnn  27372  2sqreuoplt  27373  2sqreuopltb  27374  2sqreuopnnlt  27375  2sqreuopnnltb  27376  dchrisumlem3  27400  dchrmusumlema  27402  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumlema  27409  dchrvmasumiflem1  27410  dchrisum0flblem2  27418  dchrisum0flb  27419  dchrisum0lema  27423  dchrisum0lem1b  27424  dchrisum0lem2  27427  pntrlog2bndlem2  27487  pntibndlem2  27500  pntlemf  27514  ostth2lem1  27527  qabvle  27534  sltval2  27566  sltres  27572  nolesgn2o  27581  nogesgn1o  27583  nodense  27602  nolt02o  27605  nogt01o  27606  noresle  27607  nosupbnd2lem1  27625  nosupbnd2  27626  noinfbnd2lem1  27640  noinfbnd2  27641  addsproplem1  27881  addsprop  27888  sltadd2im  27898  sleadd2im  27900  sleadd1  27901  sleadd2  27902  sltadd1  27904  sltsub1  27985  sltsub2  27986  sltsubsubbd  27992  sltsubsub2bd  27993  posdifsd  28006  subsge0d  28008  mulsproplemcbv  28023  mulsproplem1  28024  mulsprop  28038  slemuld  28046  sltmul1d  28081  sltmulneg1d  28084  sltmulneg2d  28085  slemul1ad  28090  zsoring  28301  pw2gt0divsd  28337  pw2ge0divsd  28338  legso  28544  iscgra  28754  isleag  28792  iseqlg  28812  brbtwn2  28850  axlowdim  28906  ewlksfval  29547  isnvlem  30554  nvtri  30614  nmlnoubi  30740  nmblolbii  30743  nmblolbi  30744  blocnilem  30748  sii  30798  ubthlem2  30815  minvecolem3  30820  minvecolem5  30825  minvecolem6  30826  norm-ii  31082  norm3dif  31094  norm3adifi  31097  bcs  31125  pjnorm  31668  pjnel  31670  nmbdoplbi  31968  nmbdoplb  31969  nmcoplb  31974  lnconi  31977  nmbdfnlb  31994  nmcfnlb  31998  pjdifnormi  32111  mdslmd2i  32274  cvmd  32280  cvexch  32318  cdj1i  32377  cdj3lem1  32378  cdj3lem2b  32381  cdj3lem3b  32384  cdj3i  32385  isoun  32644  nexple  32789  ismnt  32925  mgcmntco  32936  dfmgc2lem  32937  dfmgc2  32938  mgcf1o  32945  ischn  32948  chnltm1  32950  chnind  32953  chnub  32954  isinftm  33123  rlocaddval  33208  rlocmulval  33209  fldext2chn  33695  constrextdg2lem  33715  constrext2chn  33726  xrmulc1cn  33897  lmdvg  33920  faeval  34213  brfae  34215  inelcarsg  34279  carsgsigalem  34283  carsgclctunlem2  34287  carsgclctun  34289  hgt750lemc  34615  hgt750lemd  34616  hgt749d  34617  fineqvnttrclse  35077  sconnpht  35206  snmlval  35308  satfv1lem  35339  satfv1  35340  satfv0fun  35348  satfv0fvfmla0  35390  lediv2aALT  35654  faclim  35723  fvtransport  36010  idinside  36062  btwnconn1lem7  36071  btwnconn1lem11  36075  btwnconn1lem12  36076  ditgeq123dv  36199  cbvditgdavw2  36276  nn0prpwlem  36300  weiunlem1  36440  weiunfrlem  36442  bj-opabco  37166  poimirlem29  37633  heicant  37639  itg2addnclem  37655  itg2addnclem3  37657  itg2gt0cn  37659  ftc1anclem6  37682  ftc1anc  37685  ftc2nc  37686  dvasin  37688  areacirclem1  37692  seqpo  37731  incsequz  37732  metf1o  37739  mettrifi  37741  cntotbnd  37780  heiborlem4  37798  heiborlem6  37800  heiborlem10  37804  bfplem1  37806  bfplem2  37807  isopos  39163  oplecon3b  39183  atlatle  39303  4at2  39597  pmaple  39744  islaut  40066  lautcnvle  40072  lautco  40080  ltrncnvel  40125  cdlemeg49lebilem  40522  cdlemg17h  40651  tendoset  40742  tendotp  40744  cdlemk39s  40922  lcmineqlem23  42028  lcmineqlem  42029  intlewftc  42038  aks4d1p1p4  42048  dvle2  42049  aks4d1p8d2  42062  aks4d1p9  42065  aks4d1  42066  2ap1caineq  42122  sticksstones1  42123  sticksstones2  42124  sticksstones3  42125  sticksstones8  42130  sticksstones10  42132  sticksstones11  42133  sticksstones12a  42134  sticksstones15  42138  aks6d1c7lem3  42159  unitscyglem1  42172  brif12  42202  dvdsexpnn0  42311  dvdsexpb  42312  reltsub1  42363  irrapxlem2  42800  irrapxlem4  42802  irrapxlem5  42803  irrapxlem6  42804  pellexlem3  42808  monotuz  42918  monotoddzzfi  42919  monotoddzz  42920  jm2.17a  42937  jm2.17b  42938  rmygeid  42941  rmydioph  42991  expdiophlem1  42998  expdiophlem2  42999  ttac  43013  fnwe2lem2  43028  relexp01min  43690  cvgdvgrat  44290  relpeq1  44922  monoords  45283  supxrgelem  45321  supxrge  45322  abslt2sqd  45344  ltmulneg  45375  ltdiv23neg  45377  monoordxrv  45464  monoordxr  45465  monoord2xrv  45466  monoord2xr  45467  evthiccabs  45481  sqrlearg  45538  climinf  45591  climinff  45596  limsupres  45690  climinf2  45692  climinf2mpt  45699  climinfmpt  45700  supcnvlimsup  45725  liminfval2  45753  liminfltlem  45789  fprodsubrecnncnvlem  45892  fprodaddrecnncnvlem  45894  ioodvbdlimc1lem1  45916  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  iblspltprt  45958  itgspltprt  45964  stoweidlem3  45988  fourierdlem2  46094  fourierdlem3  46095  fourierdlem11  46103  fourierdlem12  46104  fourierdlem15  46107  fourierdlem34  46126  fourierdlem41  46133  fourierdlem48  46139  fourierdlem49  46140  fourierdlem79  46170  fourierdlem83  46174  fourierdlem89  46180  fourierdlem91  46182  fourierdlem100  46191  fourierdlem107  46198  fourierdlem109  46200  fourierdlem112  46203  etransclem31  46250  etransclem32  46251  rrndistlt  46275  ioorrnopn  46290  ioorrnopnxrlem  46291  sge0less  46377  sge0le  46392  sge0split  46394  sge0lempt  46395  sge0iunmptlemre  46400  sge0isum  46412  sge0seq  46431  meaiuninclem  46465  meaiininclem  46471  meaiininc  46472  isome  46479  omeunile  46490  omeiunlempt  46505  carageniuncllem2  46507  0ome  46514  isomenndlem  46515  isomennd  46516  ovnssle  46546  ovnsubadd  46557  hsphoidmvle2  46570  hsphoidmvle  46571  hoidmvval0  46572  hoidmv1lelem1  46576  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmv1le  46579  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem3  46582  hoidmvlelem4  46583  hoidmvlelem5  46584  hoidmvle  46585  hoidifhspdmvle  46605  hspmbllem2  46612  hspmbl  46614  ovnsubadd2lem  46630  ovolval4lem2  46635  ovolval4  46636  ovolval5lem2  46638  vonioolem2  46666  vonioo  46667  vonicclem2  46669  vonicc  46670  smfid  46737  smflimlem3  46758  ormkglobd  46860  natglobalincr  46862  tworepnotupword  46871  squeezedltsq  46874  2elfz2melfz  47306  smonoord  47359  iccpart  47404  iccpartimp  47405  iccpartres  47406  sqrtpwpw2p  47526  grlicsym  48001  grlictr  48003  ismgmALT  48211  iscmgmALT  48212  issgrpALT  48213  iscsgrpALT  48214  lindslinindsimp2lem5  48451  rrx2plordisom  48712  aacllem  49790