Theorem breq12 5111

Description: Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)

Assertion

Ref	Expression
breq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Proof of Theorem breq12

Step	Hyp	Ref	Expression
1		breq1 5109	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2		breq2 5110	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝑅𝐶 ↔ 𝐵𝑅𝐷))
3	1, 2	sylan9bb 519	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  breq12i  5115  breq12d  5119  breqan12d  5122  rbropapd  5541  posn  5742  dfrel4  6194  dfpo2  6314  fununiq  6572  isopolem  7373  poxp  8164  soxp  8165  fnse  8174  poxp2  8184  poxp3  8191  ecopover  8867  canth2g  9175  ttrclss  9745  ttrclselem2  9751  infxpen  10117  sornom  10379  dcomex  10549  zorn2lem6  10603  brdom6disj  10635  fpwwe2  10752  rankcf  10886  ltresr  11249  ltxrlt  11404  wloglei  11872  ltxr  13268  xrltnr  13272  xrltnsym  13290  xrlttri  13292  xrlttr  13293  brfi1uzind  14677  brfi1indALT  14679  f1olecpbl  17725  isfull  18113  isfth  18117  prslem  18497  pslem  18772  dirtr  18802  xrsdsval  21744  dvcvx  26367  2sqmo  27791  2sqreultblem  27802  2sqreunnltblem  27805  2sqreuopb  27822  lesrec  28212  addsproplem2  28383  negsproplem2  28442  recut  28907  elreno2  28908  axcontlem9  29577  isrusgr  30169  wlk2f  30237  istrlson  30316  upgrwlkdvspth  30352  ispthson  30355  isspthson  30356  crctcshwlk  30438  crctcsh  30440  2pthon3v  30559  umgr2wlk  30565  0pthonv  30747  1pthon2v  30781  uhgr3cyclex  30810  brfinext  34351  finextfldext  34363  bralgext  34396  brr0d  36000  mclsppslem  36514  elfix2  36843  poimirlem10  38739  poimirlem11  38740  dvdsexpnn0  43577  monotoddzzfi  44140  or2expropbi  48307  dfatcolem  48528  sprsymrelfolem2  48778  poprelb  48809  cycldlenngric  49229  gpgprismgr4cyclex  49408  lgricngricex  49430  lindepsnlininds  49767  catprslem  50327