Theorem breq12 5114

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 5112	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
2		breq2 5113	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝑅𝐶 ↔ 𝐵𝑅𝐷))
3	1, 2	sylan9bb 518	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is used by:  breq12i  5118  breq12d  5122  breqan12d  5125  rbropapd  5547  posn  5747  dfrel4  6189  dfpo2  6297  isopolem  7343  poxp  8120  soxp  8121  fnse  8125  poxp2  8135  poxp3  8142  ecopover  8815  canth2g  9115  ttrclss  9685  ttrclselem2  9691  infxpen  10003  sornom  10265  dcomex  10435  zorn2lem6  10489  brdom6disj  10520  fpwwe2  10632  rankcf  10766  ltresr  11129  ltxrlt  11284  wloglei  11750  ltxr  13144  xrltnr  13148  xrltnsym  13166  xrlttri  13168  xrlttr  13169  brfi1uzind  14550  brfi1indALT  14552  f1olecpbl  17585  isfull  17973  isfth  17977  prslem  18357  pslem  18632  dirtr  18662  xrsdsval  21570  dvcvx  26188  2sqmo  27610  2sqreultblem  27621  2sqreunnltblem  27624  2sqreuopb  27641  lesrec  28001  addsproplem2  28172  negsproplem2  28231  recut  28696  elreno2  28697  axcontlem9  29331  isrusgr  29920  wlk2f  29988  istrlson  30063  upgrwlkdvspth  30097  ispthson  30100  isspthson  30101  crctcshwlk  30180  crctcsh  30182  2pthon3v  30301  umgr2wlk  30307  0pthonv  30489  1pthon2v  30513  uhgr3cyclex  30542  brfinext  34051  finextfldext  34063  bralgext  34096  mclsppslem  36083  fununiq  36269  elfix2  36402  poimirlem10  38309  poimirlem11  38310  dvdsexpnn0  43123  monotoddzzfi  43697  or2expropbi  47799  dfatcolem  48020  sprsymrelfolem2  48270  poprelb  48301  cycldlenngric  48721  gpgprismgr4cyclex  48900  lgricngricex  48922  lindepsnlininds  49260  catprslem  49816