Theorem breq12d 5079

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  breq123d  5080  3brtr3d  5097  3brtr4d  5098  sbcbr  5121  pocl  5481  csbcnvgALT  5755  cnvpo  6138  sbcfung  6379  isoeq1  7070  isocnv  7083  isotr  7089  caovordig  7353  caovordg  7355  caovord2d  7357  caovord  7359  ofrfval  7417  ofrval  7419  ofrfval2  7427  caofref  7435  fnwelem  7825  fundmeng  8584  xpsneng  8602  xpcomeng  8609  xpdom2g  8613  limensuc  8694  infensuc  8695  unxpdom  8725  pssnn  8736  dif1en  8751  unfilem3  8784  unfi  8785  domunfican  8791  fodomfi  8797  marypha1lem  8897  infsupprpr  8968  wemaplem1  9010  wemaplem2  9011  wemapwe  9160  dif1card  9436  infxpenlem  9439  pwsdompw  9626  infmap2  9640  sornom  9699  isfin5  9721  isfin6  9722  domtriomlem  9864  axdc2lem  9870  axdclem2  9942  pwcfsdom  10005  cfpwsdom  10006  alephom  10007  fpwwe2lem7  10058  fpwwe2lem9  10060  tskcard  10203  ordpipq  10364  adderpqlem  10376  mulerpqlem  10377  mulcanenq  10382  lterpq  10392  ltanq  10393  ltmnq  10394  ltaddnq  10396  ltrnq  10401  archnq  10402  reclem4pr  10472  ltasr  10522  sqgt0sr  10528  axpre-ltadd  10589  axpre-mulgt0  10590  ltadd1  11107  leadd2  11109  ltmul2  11491  lemul2  11493  lemul1a  11494  ltdiv1  11504  ltdiv2  11526  lediv2  11530  div4p1lem1div2  11893  nn0ledivnn  12503  xleadd1  12649  xltadd2  12651  xsubge0  12655  xlemul1a  12682  xlemul1  12684  xlemul2  12685  xltmul2  12687  ltdifltdiv  13205  fzennn  13337  monoord  13401  monoord2  13402  expmordi  13532  ltexp2r  13538  leexp1a  13540  sqlecan  13572  bernneq  13591  faclbnd  13651  faclbnd3  13653  faclbnd4lem1  13654  faclbnd4lem2  13655  faclbnd4lem3  13656  faclbnd4lem4  13657  faclbnd6  13660  facubnd  13661  rlimcld2  14935  isercoll2  15025  climsup  15026  iseraltlem2  15039  fsumabs  15156  fsumrlim  15166  climcndslem1  15204  climcndslem2  15205  supcvg  15211  geomulcvg  15232  cvgrat  15239  ntrivcvgtail  15256  ruclem2  15585  ruclem8  15590  addmodlteqALT  15675  fproddvdsd  15684  sadcaddlem  15806  sadcadd  15807  nn0seqcvgd  15914  algcvg  15920  algcvga  15923  eucalgcvga  15930  isprm5  16051  qnumgt0  16090  pcprendvds2  16178  pcpremul  16180  pcadd2  16226  prmreclem4  16255  prmreclem5  16256  prmreclem6  16257  2expltfac  16426  xpsle  16852  mreexexlemd  16915  issubc  17105  latjlej2  17676  latmlem2  17692  sylow1lem3  18725  isslw  18733  fislw  18750  efgi  18845  lt6abl  19015  ablfac1eu  19195  isabv  19590  abvtri  19601  cayleyhamilton1  21500  isucn  22887  ispsmet  22914  psmettri2  22919  ismet  22933  isxmet  22934  xmettri2  22950  imasdsf1olem  22983  imasf1oxmet  22985  blvalps  22995  blval  22996  comet  23123  stdbdxmet  23125  nrmmetd  23184  tngngp  23263  tngngp3  23265  nmofval  23323  nmolb2d  23327  nmoi  23337  nmoix  23338  icopnfhmeo  23547  xrhmeo  23550  evth2  23564  pi1grplem  23653  minveclem6  24037  ovolfiniun  24102  ovoliunlem3  24105  voliunlem3  24153  ioombl1  24163  mbfmax  24250  mbfpos  24252  itg1climres  24315  mbfi1fseqlem2  24317  mbfi1fseqlem6  24321  mbfi1fseq  24322  mbfmullem  24326  itg2split  24350  itg2monolem1  24351  itg2monolem3  24353  itg2mono  24354  itg2i1fseqle  24355  itg2i1fseq  24356  itg2i1fseq2  24357  itg2addlem  24359  rolle  24587  dvlip  24590  c1lip1  24594  dvcnvrelem1  24614  dvcvx  24617  ply1divex  24730  q1pval  24747  fta1glem2  24760  fta1g  24761  fta1b  24763  plydivlem3  24884  fta1lem  24896  fta1  24897  aalioulem3  24923  aalioulem4  24924  aaliou3lem2  24932  aaliou3lem8  24934  aaliou3lem9  24939  ulmdvlem1  24988  ulmdvlem3  24990  abelthlem2  25020  abelthlem7a  25025  argrege0  25194  cxplt  25277  cxplea  25279  cxple2  25280  cxplt3  25283  logbleb  25361  logblt  25362  rlimcxp  25551  scvxcvx  25563  jensenlem2  25565  ftalem3  25652  ftalem7  25656  vmalelog  25781  chtub  25788  chpchtsum  25795  bclbnd  25856  efexple  25857  bposlem5  25864  bposlem6  25865  bposlem7  25866  lgsdilem  25900  2lgslem1a2  25966  2sqreuop  26038  2sqreuopnn  26039  2sqreuoplt  26040  2sqreuopltb  26041  2sqreuopnnlt  26042  2sqreuopnnltb  26043  dchrisumlem3  26067  dchrmusumlema  26069  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumlema  26076  dchrvmasumiflem1  26077  dchrisum0flblem2  26085  dchrisum0flb  26086  dchrisum0lema  26090  dchrisum0lem1b  26091  dchrisum0lem2  26094  pntrlog2bndlem2  26154  pntibndlem2  26167  pntlemf  26181  ostth2lem1  26194  qabvle  26201  legso  26385  iscgra  26595  isleag  26633  iseqlg  26653  brbtwn2  26691  axlowdim  26747  ewlksfval  27383  isnvlem  28387  nvtri  28447  nmlnoubi  28573  nmblolbii  28576  nmblolbi  28577  blocnilem  28581  sii  28631  ubthlem2  28648  minvecolem3  28653  minvecolem5  28658  minvecolem6  28659  norm-ii  28915  norm3dif  28927  norm3adifi  28930  bcs  28958  pjnorm  29501  pjnel  29503  nmbdoplbi  29801  nmbdoplb  29802  nmcoplb  29807  lnconi  29810  nmbdfnlb  29827  nmcfnlb  29831  pjdifnormi  29944  mdslmd2i  30107  cvmd  30113  cvexch  30151  cdj1i  30210  cdj3lem1  30211  cdj3lem2b  30214  cdj3lem3b  30217  cdj3i  30218  isoun  30437  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  34936  heicant  34942  itg2addnclem  34958  itg2addnclem3  34960  itg2gt0cn  34962  ftc1anclem6  34987  ftc1anc  34990  ftc2nc  34991  dvasin  34993  areacirclem1  34997  seqpo  35037  incsequz  35038  metf1o  35045  mettrifi  35047  cntotbnd  35089  heiborlem4  35107  heiborlem6  35109  heiborlem10  35113  bfplem1  35115  bfplem2  35116  isopos  36331  oplecon3b  36351  atlatle  36471  4at2  36765  pmaple  36912  islaut  37234  lautcnvle  37240  lautco  37248  ltrncnvel  37293  cdlemeg49lebilem  37690  cdlemg17h  37819  tendoset  37910  tendotp  37912  cdlemk39s  38090  factwoffsmonot  39147  reltsub1  39265  irrapxlem2  39469  irrapxlem4  39471  irrapxlem5  39472  irrapxlem6  39473  pellexlem3  39477  monotuz  39587  monotoddzzfi  39588  monotoddzz  39589  jm2.17a  39606  jm2.17b  39607  rmygeid  39610  rmydioph  39660  expdiophlem1  39667  expdiophlem2  39668  ttac  39682  fnwe2lem2  39700  relexp01min  40107  cvgdvgrat  40694  monoords  41613  supxrgelem  41654  supxrge  41655  abslt2sqd  41677  ltmulneg  41713  ltdiv23neg  41715  monoordxrv  41807  monoordxr  41808  monoord2xrv  41809  monoord2xr  41810  evthiccabs  41820  sqrlearg  41878  climinf  41936  climinff  41941  limsupres  42035  climinf2  42037  climinf2mpt  42044  climinfmpt  42045  supcnvlimsup  42070  liminfval2  42098  liminflelimsuplem  42105  liminfltlem  42134  fprodsubrecnncnvlem  42240  fprodaddrecnncnvlem  42242  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  iblspltprt  42307  itgspltprt  42313  stoweidlem3  42337  fourierdlem2  42443  fourierdlem3  42444  fourierdlem11  42452  fourierdlem12  42453  fourierdlem15  42456  fourierdlem34  42475  fourierdlem41  42482  fourierdlem48  42488  fourierdlem49  42489  fourierdlem79  42519  fourierdlem83  42523  fourierdlem89  42529  fourierdlem91  42531  fourierdlem100  42540  fourierdlem107  42547  fourierdlem109  42549  fourierdlem112  42552  etransclem31  42599  etransclem32  42600  rrndistlt  42624  ioorrnopn  42639  ioorrnopnxrlem  42640  sge0less  42723  sge0le  42738  sge0split  42740  sge0lempt  42741  sge0iunmptlemre  42746  sge0isum  42758  sge0seq  42777  meaiuninclem  42811  meaiininclem  42817  meaiininc  42818  isome  42825  omeunile  42836  omeiunlempt  42851  carageniuncllem2  42853  0ome  42860  isomenndlem  42861  isomennd  42862  ovnsslelem  42891  ovnssle  42892  ovnsubadd  42903  hsphoidmvle2  42916  hsphoidmvle  42917  hoidmvval0  42918  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  hoidmvlelem5  42930  hoidmvle  42931  hoidifhspdmvle  42951  hspmbllem2  42958  hspmbl  42960  ovnsubadd2lem  42976  ovolval4lem2  42981  ovolval4  42982  ovolval5lem2  42984  vonioolem2  43012  vonioo  43013  vonicclem2  43015  vonicc  43016  smfid  43078  smflimlem3  43098  2elfz2melfz  43567  smonoord  43580  iccpart  43625  iccpartimp  43626  iccpartres  43627  sqrtpwpw2p  43749  ismgmALT  44179  iscmgmALT  44180  issgrpALT  44181  iscsgrpALT  44182  lindslinindsimp2lem5  44566  rrx2plordisom  44759  aacllem  44951