Theorem breq12d 4868

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637   class class class wbr 4855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856

This theorem is referenced by:  breq123d  4869  3brtr3d  4886  3brtr4d  4887  sbcbr  4910  pocl  5252  csbcnvgALT  5521  cnvpo  5900  sbcfung  6134  isoeq1  6800  isocnv  6813  isotr  6819  caovordig  7078  caovordg  7080  caovord2d  7082  caovord  7084  ofrfval  7144  ofrval  7146  ofrfval2  7154  caofref  7162  fnwelem  7535  fundmeng  8276  xpsneng  8293  xpcomeng  8300  xpdom2g  8304  limensuc  8385  infensuc  8386  unxpdom  8415  pssnn  8426  dif1en  8441  unfilem3  8474  unfi  8475  domunfican  8481  fodomfi  8487  marypha1lem  8587  wemaplem1  8699  wemaplem2  8700  wemapwe  8850  dif1card  9125  infxpenlem  9128  pwsdompw  9320  infmap2  9334  sornom  9393  isfin5  9415  isfin6  9416  domtriomlem  9558  axdc2lem  9564  axdclem2  9636  pwcfsdom  9699  cfpwsdom  9700  alephom  9701  fpwwe2lem7  9752  fpwwe2lem9  9754  tskcard  9897  ordpipq  10058  adderpqlem  10070  mulerpqlem  10071  mulcanenq  10076  lterpq  10086  ltanq  10087  ltmnq  10088  ltaddnq  10090  ltrnq  10095  archnq  10096  reclem4pr  10166  ltasr  10215  sqgt0sr  10221  axpre-ltadd  10282  axpre-mulgt0  10283  ltadd1  10789  leadd2  10791  ltmul2  11168  lemul2  11170  lemul1a  11171  ltdiv1  11181  ltdiv2  11203  lediv2  11207  div4p1lem1div2  11573  nn0ledivnn  12176  xleadd1  12322  xltadd2  12324  xsubge0  12328  xlemul1a  12355  xlemul1  12357  xlemul2  12358  xltmul2  12360  ltdifltdiv  12878  fzennn  13010  monoord  13073  monoord2  13074  ltexp2r  13159  leexp1a  13161  sqlecan  13213  bernneq  13232  faclbnd  13316  faclbnd3  13318  faclbnd4lem1  13319  faclbnd4lem2  13320  faclbnd4lem3  13321  faclbnd4lem4  13322  faclbnd6  13325  facubnd  13326  rlimcld2  14551  isercoll2  14641  climsup  14642  iseraltlem2  14655  fsumabs  14774  fsumrlim  14784  climcndslem1  14822  climcndslem2  14823  supcvg  14829  geomulcvg  14848  cvgrat  14855  ntrivcvgtail  14872  fprodle  14966  ruclem2  15200  ruclem8  15205  addmodlteqALT  15289  fproddvdsd  15298  sadcaddlem  15417  sadcadd  15418  nn0seqcvgd  15521  algcvg  15527  algcvga  15530  eucalgcvga  15537  isprm5  15655  qnumgt0  15694  pcprendvds2  15782  pcpremul  15784  pcadd2  15830  prmreclem4  15859  prmreclem5  15860  prmreclem6  15861  2expltfac  16030  xpsle  16465  mreexexlemd  16528  issubc  16718  latjlej2  17290  latmlem2  17306  sylow1lem3  18235  isslw  18243  fislw  18260  efgi  18352  lt6abl  18516  ablfac1eu  18693  isabv  19042  abvtri  19053  cayleyhamilton1  20930  isucn  22315  ispsmet  22342  psmettri2  22347  ismet  22361  isxmet  22362  xmettri2  22378  imasdsf1olem  22411  imasf1oxmet  22413  blvalps  22423  blval  22424  comet  22551  stdbdxmet  22553  nrmmetd  22612  tngngp  22691  tngngp3  22693  nmofval  22751  nmolb2d  22755  nmoi  22765  nmoix  22766  icopnfhmeo  22975  xrhmeo  22978  evth2  22992  pi1grplem  23081  minveclem6  23439  ovolfiniun  23504  ovoliunlem3  23507  voliunlem3  23555  ioombl1  23565  mbfmax  23652  mbfpos  23654  itg1climres  23717  mbfi1fseqlem2  23719  mbfi1fseqlem6  23723  mbfi1fseq  23724  mbfmullem  23728  itg2split  23752  itg2monolem1  23753  itg2monolem3  23755  itg2mono  23756  itg2i1fseqle  23757  itg2i1fseq  23758  itg2i1fseq2  23759  itg2addlem  23761  rolle  23989  dvlip  23992  c1lip1  23996  dvcnvrelem1  24016  dvcvx  24019  ply1divex  24132  q1pval  24149  fta1glem2  24162  fta1g  24163  fta1b  24165  plydivlem3  24286  fta1lem  24298  fta1  24299  aalioulem3  24325  aalioulem4  24326  aaliou3lem2  24334  aaliou3lem8  24336  aaliou3lem9  24341  ulmdvlem1  24390  ulmdvlem3  24392  abelthlem2  24422  abelthlem7a  24427  argrege0  24593  cxplt  24676  cxplea  24678  cxple2  24679  cxplt3  24682  logbleb  24757  logblt  24758  rlimcxp  24936  scvxcvx  24948  jensenlem2  24950  ftalem3  25037  ftalem7  25041  vmalelog  25166  chtub  25173  chpchtsum  25180  bclbnd  25241  efexple  25242  bposlem5  25249  bposlem6  25250  bposlem7  25251  lgsdilem  25285  2lgslem1a2  25351  dchrisumlem3  25416  dchrmusumlema  25418  dchrmusum2  25419  dchrvmasumlem2  25423  dchrvmasumlema  25425  dchrvmasumiflem1  25426  dchrisum0flblem2  25434  dchrisum0flb  25435  dchrisum0lema  25439  dchrisum0lem1b  25440  dchrisum0lem2  25443  pntrlog2bndlem2  25503  pntibndlem2  25516  pntlemf  25530  ostth2lem1  25543  qabvle  25550  legso  25730  iscgra  25937  isleag  25969  iseqlg  25983  brbtwn2  26021  axlowdim  26077  ewlksfval  26747  isnvlem  27815  nvtri  27875  nmlnoubi  28001  nmblolbii  28004  nmblolbi  28005  blocnilem  28009  sii  28059  ubthlem2  28077  minvecolem3  28082  minvecolem5  28087  minvecolem6  28088  norm-ii  28345  norm3dif  28357  norm3adifi  28360  bcs  28388  pjnorm  28933  pjnel  28935  nmbdoplbi  29233  nmbdoplb  29234  nmcoplb  29239  lnconi  29242  nmbdfnlb  29259  nmcfnlb  29263  pjdifnormi  29376  mdslmd2i  29539  cvmd  29545  cvexch  29583  cdj1i  29642  cdj3lem1  29643  cdj3lem2b  29646  cdj3lem3b  29649  cdj3i  29650  isoun  29828  isomnd  30048  omndadd  30053  omndmul  30061  ogrpinvlt  30071  isinftm  30082  gsumle  30126  xrmulc1cn  30323  lmdvg  30346  nexple  30418  faeval  30656  brfae  30658  inelcarsg  30720  carsgsigalem  30724  carsgclctunlem2  30728  carsgclctun  30730  hgt750lemc  31072  hgt750lemd  31073  hgt749d  31074  sconnpht  31555  snmlval  31657  lediv2aALT  31914  faclim  31975  poseq  32095  sltval2  32151  sltres  32157  nolesgn2o  32166  nodense  32184  nolt02o  32187  noresle  32188  nosupbnd2lem1  32203  nosupbnd2  32204  fvtransport  32481  idinside  32533  btwnconn1lem7  32542  btwnconn1lem11  32546  btwnconn1lem12  32547  nn0prpwlem  32659  poimirlem29  33769  heicant  33775  itg2addnclem  33791  itg2addnclem3  33793  itg2gt0cn  33795  ftc1anclem6  33820  ftc1anc  33823  ftc2nc  33824  dvasin  33826  areacirclem1  33830  seqpo  33872  incsequz  33873  metf1o  33880  mettrifi  33882  cntotbnd  33924  heiborlem4  33942  heiborlem6  33944  heiborlem10  33948  bfplem1  33950  bfplem2  33951  isopos  34978  oplecon3b  34998  atlatle  35118  4at2  35412  pmaple  35559  islaut  35881  lautcnvle  35887  lautco  35895  ltrncnvel  35940  cdlemeg49lebilem  36337  cdlemg17h  36466  tendoset  36557  tendotp  36559  cdlemk39s  36737  irrapxlem2  37906  irrapxlem4  37908  irrapxlem5  37909  irrapxlem6  37910  pellexlem3  37914  monotuz  38024  monotoddzzfi  38025  monotoddzz  38026  expmordi  38030  jm2.17a  38045  jm2.17b  38046  rmygeid  38049  rmydioph  38099  expdiophlem1  38106  expdiophlem2  38107  ttac  38121  fnwe2lem2  38139  relexp01min  38522  cvgdvgrat  39029  monoords  40009  supxrgelem  40050  supxrge  40051  abslt2sqd  40073  ltmulneg  40111  ltdiv23neg  40113  monoordxrv  40208  monoordxr  40209  monoord2xrv  40210  monoord2xr  40211  evthiccabs  40219  sqrlearg  40277  climinf  40335  climinff  40340  limsupres  40434  climinf2  40436  climinf2mpt  40443  climinfmpt  40444  supcnvlimsup  40469  liminfval2  40497  liminflelimsuplem  40504  liminfltlem  40533  fprodsubrecnncnvlem  40618  fprodaddrecnncnvlem  40620  ioodvbdlimc1lem1  40643  ioodvbdlimc1lem2  40644  ioodvbdlimc2lem  40646  iblspltprt  40685  itgspltprt  40691  stoweidlem3  40716  fourierdlem2  40822  fourierdlem3  40823  fourierdlem11  40831  fourierdlem12  40832  fourierdlem15  40835  fourierdlem34  40854  fourierdlem41  40861  fourierdlem48  40867  fourierdlem49  40868  fourierdlem79  40898  fourierdlem83  40902  fourierdlem89  40908  fourierdlem91  40910  fourierdlem100  40919  fourierdlem107  40926  fourierdlem109  40928  fourierdlem112  40931  etransclem31  40978  etransclem32  40979  rrndistlt  41006  ioorrnopn  41021  ioorrnopnxrlem  41022  sge0less  41105  sge0le  41120  sge0split  41122  sge0lempt  41123  sge0iunmptlemre  41128  sge0isum  41140  sge0seq  41159  meaiuninclem  41193  meaiininclem  41199  meaiininc  41200  isome  41207  omeunile  41218  omeiunlempt  41233  carageniuncllem2  41235  0ome  41242  isomenndlem  41243  isomennd  41244  ovnsslelem  41273  ovnssle  41274  ovnsubadd  41285  hsphoidmvle2  41298  hsphoidmvle  41299  hoidmvval0  41300  hoidmv1lelem1  41304  hoidmv1lelem2  41305  hoidmv1lelem3  41306  hoidmv1le  41307  hoidmvlelem1  41308  hoidmvlelem2  41309  hoidmvlelem3  41310  hoidmvlelem4  41311  hoidmvlelem5  41312  hoidmvle  41313  hoidifhspdmvle  41333  hspmbllem2  41340  hspmbl  41342  ovnsubadd2lem  41358  ovolval4lem2  41363  ovolval4  41364  ovolval5lem2  41366  vonioolem2  41394  vonioo  41395  vonicclem2  41397  vonicc  41398  smfid  41460  smflimlem3  41480  2elfz2melfz  41920  smonoord  41933  iccpart  41944  iccpartimp  41945  iccpartres  41946  sqrtpwpw2p  42042  ismgmALT  42444  iscmgmALT  42445  issgrpALT  42446  iscsgrpALT  42447  lindslinindsimp2lem5  42836  aacllem  43135