Theorem breq12 4658

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

Assertion

Ref	Expression
breq12	|- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )

Proof of Theorem breq12

Step	Hyp	Ref	Expression
1		breq1 4656	. 2 |- ( A = B -> ( A R C <-> B R C ) )
2		breq2 4657	. 2 |- ( C = D -> ( B R C <-> B R D ) )
3	1, 2	sylan9bb 736	1 |- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  breq12i  4662  breq12d  4666  breqan12d  4669  rbropapd  5015  posn  5187  dfrel4  5585  isopolem  6595  poxp  7289  soxp  7290  fnse  7294  ecopover  7851  ecopoverOLD  7852  canth2g  8114  infxpen  8837  sornom  9099  dcomex  9269  zorn2lem6  9323  brdom6disj  9354  fpwwe2  9465  rankcf  9599  ltresr  9961  ltxrlt  10108  wloglei  10560  ltxr  11949  xrltnr  11953  xrltnsym  11970  xrlttri  11972  xrlttr  11973  brfi1uzind  13280  brfi1indALT  13282  brfi1uzindOLD  13286  brfi1indALTOLD  13288  f1olecpbl  16187  isfull  16570  isfth  16574  prslem  16931  pslem  17206  dirtr  17236  xrsdsval  19790  dvcvx  23783  axcontlem9  25852  isrusgr  26457  wlk2f  26525  istrlson  26603  upgrwlkdvspth  26635  ispthson  26638  isspthson  26639  crctcshwlk  26714  crctcsh  26716  2pthon3v  26839  umgr2wlk  26845  0pthonv  26990  1pthon2v  27013  uhgr3cyclex  27042  2sqmo  29649  mclsppslem  31480  dfpo2  31645  fununiq  31667  slerec  31923  elfix2  32011  poimirlem10  33419  poimirlem11  33420  monotoddzzfi  37507  sprsymrelfolem2  41743  lindepsnlininds  42241