Theorem breq2 4097

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq2	⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 3868	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	eleq1d 2300	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3		df-br 4094	. 2 ⊢ (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4		df-br 4094	. 2 ⊢ (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2202  ⟨cop 3676   class class class wbr 4093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  breq12  4098  breq2i  4101  breq2d  4105  nbrne1  4112  brralrspcev  4152  brimralrspcev  4153  pocl  4406  swopolem  4408  swopo  4409  sowlin  4423  sotricim  4426  sotritrieq  4428  seex  4438  frind  4455  wetriext  4681  vtoclr  4780  posng  4804  brcog  4903  brcogw  4905  opelcnvg  4916  dfdmf  4930  breldmg  4943  dfrnf  4979  dmcoss  5008  resieq  5029  dfres2  5071  elimag  5086  elrelimasn  5109  elimasn  5110  intirr  5130  poirr2  5136  poltletr  5144  dffun6f  5346  dffun4f  5349  fun11  5404  brprcneu  5641  fv3  5671  tz6.12c  5678  relelfvdm  5680  fvmbr  5683  funbrfv  5691  fnbrfvb  5693  funfvdm2f  5720  fndmdif  5761  dff3im  5800  fmptco  5821  foeqcnvco  5941  isorel  5959  isocnv  5962  isotr  5967  isopolem  5973  isosolem  5975  f1oiso  5977  f1oiso2  5978  caovordig  6198  caovordg  6200  caovord  6204  caofrss  6276  caoftrn  6277  poxp  6406  tposoprab  6489  ertr  6760  ecopovsym  6843  ecopovtrn  6844  ecopovsymg  6846  ecopovtrng  6847  th3qlem2  6850  domeng  6966  eqeng  6982  snfig  7032  nneneq  7086  nnfi  7102  ssfilem  7105  ssfilemd  7107  domfiexmid  7110  dif1enen  7112  diffitest  7119  findcard  7120  findcard2  7121  findcard2s  7122  diffisn  7125  tridc  7132  fimax2gtrilemstep  7133  inffiexmid  7141  unsnfi  7154  fiintim  7166  fisseneq  7170  isbth  7209  supmoti  7252  eqsupti  7255  supubti  7258  suplubti  7259  suplub2ti  7260  supmaxti  7263  supsnti  7264  isotilem  7265  isoti  7266  supisolem  7267  supisoex  7268  cardcl  7445  isnumi  7446  cardval3ex  7449  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidapne  7539  nqtri3or  7676  ltsonq  7678  ltanqg  7680  ltmnqg  7681  ltexnqq  7688  nsmallnqq  7692  subhalfnqq  7694  ltbtwnnqq  7695  prarloclemarch2  7699  nqnq0pi  7718  prcdnql  7764  prcunqu  7765  prnminu  7769  genpcdl  7799  genprndl  7801  genprndu  7802  genpdisj  7803  nqprm  7822  nqprrnd  7823  nqprdisj  7824  nqprloc  7825  nqprlu  7827  nqprl  7831  addnqprlemru  7838  addnqprlemfl  7839  addnqprlemfu  7840  mulnqprlemru  7854  mulnqprlemfl  7855  mulnqprlemfu  7856  1idpru  7871  ltnqpr  7873  ltnqpri  7874  prplnqu  7900  recexprlemelu  7903  recexprlemm  7904  recexprlemloc  7911  recexprlem1ssl  7913  recexprlemss1u  7916  cauappcvgprlemm  7925  cauappcvgprlemopu  7928  cauappcvgprlemupu  7929  cauappcvgprlemdisj  7931  cauappcvgprlemloc  7932  cauappcvgprlemladdfu  7934  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem2  7940  caucvgprlemnkj  7946  caucvgprlemnbj  7947  caucvgprlemm  7948  caucvgprlemopu  7951  caucvgprlemupu  7952  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprlemcl  7956  caucvgprlemladdfu  7957  caucvgprlemladdrl  7958  caucvgprlem2  7960  caucvgprprlemelu  7966  caucvgprprlemcbv  7967  caucvgprprlemval  7968  caucvgprprlemnbj  7973  caucvgprprlemmu  7975  caucvgprprlemexbt  7986  caucvgprprlemaddq  7988  caucvgprprlem1  7989  caucvgprprlem2  7990  suplocexprlemmu  7998  suplocexprlemru  7999  suplocexprlemdisj  8000  suplocexprlemloc  8001  suplocexprlemub  8003  suplocexpr  8005  lttrsr  8042  ltsosr  8044  ltasrg  8050  recexgt0sr  8053  mulgt0sr  8058  aptisr  8059  mulextsr1  8061  srpospr  8063  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  caucvgsr  8082  map2psrprg  8085  suplocsrlemb  8086  suplocsrlempr  8087  suplocsrlem  8088  axprecex  8160  axpre-ltwlin  8163  axpre-lttrn  8164  axpre-apti  8165  axpre-ltadd  8166  axpre-mulgt0  8167  axpre-mulext  8168  axcaucvglemcau  8178  axcaucvglemres  8179  axcaucvg  8180  axpre-suploclemres  8181  axpre-suploc  8182  ltxrlt  8304  lttri3  8318  ltne  8323  eqle  8330  ltordlem  8721  reapti  8818  apreim  8842  squeeze0  9143  lbreu  9184  lble  9186  suprleubex  9193  sup3exmid  9196  nnge1  9225  nn2ge  9235  nn1gt1  9236  nnsub  9241  nominpos  9441  nn0ge0  9486  elnnnn0b  9505  nn0ge2m1nn  9523  zdclt  9618  suprzclex  9639  peano2uz2  9648  peano5uzti  9649  dfuzi  9651  uzind  9652  uzind3  9654  eluz1  9820  uzind4  9883  indstr  9888  supinfneg  9890  infsupneg  9891  infregelbex  9893  indstr2  9904  ublbneg  9908  irrmulap  9943  elpq  9944  elpqb  9945  elrp  9951  mnfltxr  10082  nn0pnfge0  10087  xrltnsym  10089  xrlttr  10091  xrltso  10092  xrlttri3  10093  xrltne  10109  ngtmnft  10113  nmnfgt  10114  xrrebnd  10115  z2ge  10122  xltnegi  10131  xltadd1  10172  xsubge0  10177  xleaddadd  10183  ixxval  10192  elixx1  10193  elioo2  10217  iccid  10221  iccsupr  10262  repos  10266  fzval  10307  elfz1  10310  fzm1  10397  zsupcllemstep  10552  suprzubdc  10559  zsupssdc  10561  qdclt  10568  exbtwnzlemstep  10570  exbtwnzlemex  10572  qbtwnre  10579  qbtwnxr  10580  flval  10595  apbtwnz  10597  modqid2  10676  modqmuladdnn0  10693  exp3val  10866  expge0  10900  expge1  10901  nn0ltexp2  11034  facdiv  11063  facwordi  11065  hashinfom  11103  hashennn  11105  hashunlem  11130  zfz1iso  11168  wrdlen1  11217  fstwrdne0  11219  wrdl1exs1  11272  pfxsuffeqwrdeq  11345  pfxsuff1eqwrdeq  11346  ccats1pfxeq  11361  ccats1pfxeqrex  11362  pfxccatin12lem3  11379  ovshftex  11459  shftfibg  11460  shftfib  11463  shftfn  11464  2shfti  11471  sqrt0rlem  11643  resqrexlemex  11665  rsqrmo  11667  resqrtcl  11669  rersqrtthlem  11670  sqrtsq  11684  cau3lem  11754  caubnd2  11757  maxleim  11845  maxabslemval  11848  maxleast  11853  maxleb  11856  fimaxre2  11867  minmax  11870  xrmaxleim  11884  xrmaxiflemval  11890  xrmaxaddlem  11900  xrminmax  11905  xrbdtri  11916  climi  11927  climeu  11936  climmo  11938  2clim  11941  addcn2  11950  mulcn2  11952  reccn2ap  11953  cn1lem  11954  summodc  12024  zsumdc  12025  fsum3  12028  cvgratz  12173  ntrivcvgap0  12190  prodmodc  12219  zproddc  12220  fprodseq  12224  fprodntrivap  12225  sinltxirr  12402  dvdsabsb  12451  0dvds  12452  alzdvds  12495  dvdsext  12496  fzo0dvdseq  12498  2tp1odd  12525  2teven  12528  divalglemnn  12559  divalglemeunn  12562  divalglemeuneg  12564  bitsinv1lem  12602  gcdval  12610  gcddvds  12614  bezoutlemstep  12648  bezoutlemmain  12649  bezoutlemex  12652  bezoutlemeu  12658  bezoutlemsup  12660  dfgcd3  12661  bezout  12662  dvdsgcd  12663  dfgcd2  12665  dvdssq  12682  uzwodc  12688  nnwofdc  12689  lcmval  12715  lcmcllem  12719  dvdslcm  12721  lcmledvds  12722  lcmgcdlem  12729  lcmdvds  12731  coprmgcdb  12740  coprmdvds2  12745  cncongr1  12755  cncongr2  12756  isprm  12761  dvdsnprmd  12777  dvdsprm  12789  exprmfct  12790  isprm6  12799  prmexpb  12803  prmfac1  12804  rpexp  12805  sqrt2irr  12814  oddpwdclemdc  12825  oddpwdc  12826  sqpweven  12827  2sqpwodd  12828  sqne2sq  12829  nnoddn2prmb  12915  pceu  12948  pczpre  12950  pcdiv  12955  pcdvdsb  12973  difsqpwdvds  12991  pcmpt  12996  pcmptdvds  12998  oddprmdvds  13007  prmpwdvds  13008  infpnlem2  13013  oddennn  13093  evenennn  13094  exmidunben  13127  nninfdclemcl  13149  nninfdclemp1  13151  nninfdc  13154  infpn2  13157  eqgen  13894  zndvds  14745  znleval  14749  comet  15310  metcnpi  15326  metcnpi2  15327  metcnpi3  15328  addcncntoplem  15372  cncfi  15389  elcncf1di  15390  mulcncflem  15418  dedekindeulemuub  15428  dedekindeulemloc  15430  dedekindeulemlu  15432  dedekindeulemeu  15433  dedekindeu  15434  suplociccreex  15435  suplociccex  15436  dedekindicclemuub  15437  dedekindicclemloc  15439  dedekindicclemlu  15441  dedekindicclemeu  15442  dedekindicclemicc  15443  dedekindicc  15444  ivthinclemlopn  15447  ivthinclemlr  15448  ivthinclemuopn  15449  ivthinclemur  15450  ivthinclemloc  15452  ivthinc  15454  ivthreinc  15456  dich0  15463  ivthdich  15464  limcimo  15476  cnplimclemr  15480  limccnp2lem  15487  limccoap  15489  eldvap  15493  logltb  15685  pellexlem3  15793  lgsdir  15854  lgsne0  15857  gausslemma2dlem0i  15876  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  2lgslem2  15911  2lgs  15923  2sqlem6  15939  2sqlem8  15942  2sqlem10  15944  lfgredg2dom  16073  istrl  16326  clwwlkn0  16349  clwwlkext2edg  16363  clwwlknonccat  16374  clwwlknonex2  16380  iseupth  16388  konigsberg  16434  sbthom  16754  trilpo  16775  trirec0  16776  apdiff  16780  reap0  16791  cndcap  16792  nconstwlpolem  16798  neapmkv  16801  neap0mkv  16802  ltlenmkv  16803