Theorem breq2 4087

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 3858	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	eleq1d 2298	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3		df-br 4084	. 2 ⊢ (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4		df-br 4084	. 2 ⊢ (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ⟨cop 3669   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breq12  4088  breq2i  4091  breq2d  4095  nbrne1  4102  brralrspcev  4142  brimralrspcev  4143  pocl  4394  swopolem  4396  swopo  4397  sowlin  4411  sotricim  4414  sotritrieq  4416  seex  4426  frind  4443  wetriext  4669  vtoclr  4767  posng  4791  brcog  4889  brcogw  4891  opelcnvg  4902  dfdmf  4916  breldmg  4929  dfrnf  4965  dmcoss  4994  resieq  5015  dfres2  5057  elimag  5072  elrelimasn  5094  elimasn  5095  intirr  5115  poirr2  5121  poltletr  5129  dffun6f  5331  dffun4f  5334  fun11  5388  brprcneu  5622  fv3  5652  tz6.12c  5659  relelfvdm  5661  fvmbr  5664  funbrfv  5672  fnbrfvb  5674  funfvdm2f  5701  fndmdif  5742  dff3im  5782  fmptco  5803  foeqcnvco  5920  isorel  5938  isocnv  5941  isotr  5946  isopolem  5952  isosolem  5954  f1oiso  5956  f1oiso2  5957  caovordig  6177  caovordg  6179  caovord  6183  caofrss  6256  caoftrn  6257  poxp  6384  tposoprab  6432  ertr  6703  ecopovsym  6786  ecopovtrn  6787  ecopovsymg  6789  ecopovtrng  6790  th3qlem2  6793  domeng  6909  eqeng  6925  snfig  6975  nneneq  7026  nnfi  7042  ssfilem  7045  domfiexmid  7048  dif1enen  7050  diffitest  7057  findcard  7058  findcard2  7059  findcard2s  7060  diffisn  7063  tridc  7070  fimax2gtrilemstep  7071  inffiexmid  7079  unsnfi  7092  fiintim  7104  fisseneq  7107  isbth  7145  supmoti  7171  eqsupti  7174  supubti  7177  suplubti  7178  suplub2ti  7179  supmaxti  7182  supsnti  7183  isotilem  7184  isoti  7185  supisolem  7186  supisoex  7187  cardcl  7364  isnumi  7365  cardval3ex  7368  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidapne  7457  nqtri3or  7594  ltsonq  7596  ltanqg  7598  ltmnqg  7599  ltexnqq  7606  nsmallnqq  7610  subhalfnqq  7612  ltbtwnnqq  7613  prarloclemarch2  7617  nqnq0pi  7636  prcdnql  7682  prcunqu  7683  prnminu  7687  genpcdl  7717  genprndl  7719  genprndu  7720  genpdisj  7721  nqprm  7740  nqprrnd  7741  nqprdisj  7742  nqprloc  7743  nqprlu  7745  nqprl  7749  addnqprlemru  7756  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemru  7772  mulnqprlemfl  7773  mulnqprlemfu  7774  1idpru  7789  ltnqpr  7791  ltnqpri  7792  prplnqu  7818  recexprlemelu  7821  recexprlemm  7822  recexprlemloc  7829  recexprlem1ssl  7831  recexprlemss1u  7834  cauappcvgprlemm  7843  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfu  7852  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem2  7858  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem2  7878  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnbj  7891  caucvgprprlemmu  7893  caucvgprprlemexbt  7904  caucvgprprlemaddq  7906  caucvgprprlem1  7907  caucvgprprlem2  7908  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  suplocexpr  7923  lttrsr  7960  ltsosr  7962  ltasrg  7968  recexgt0sr  7971  mulgt0sr  7976  aptisr  7977  mulextsr1  7979  srpospr  7981  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  caucvgsr  8000  map2psrprg  8003  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axprecex  8078  axpre-ltwlin  8081  axpre-lttrn  8082  axpre-apti  8083  axpre-ltadd  8084  axpre-mulgt0  8085  axpre-mulext  8086  axcaucvglemcau  8096  axcaucvglemres  8097  axcaucvg  8098  axpre-suploclemres  8099  axpre-suploc  8100  ltxrlt  8223  lttri3  8237  ltne  8242  eqle  8249  ltordlem  8640  reapti  8737  apreim  8761  squeeze0  9062  lbreu  9103  lble  9105  suprleubex  9112  sup3exmid  9115  nnge1  9144  nn2ge  9154  nn1gt1  9155  nnsub  9160  nominpos  9360  nn0ge0  9405  elnnnn0b  9424  nn0ge2m1nn  9440  zdclt  9535  suprzclex  9556  peano2uz2  9565  peano5uzti  9566  dfuzi  9568  uzind  9569  uzind3  9571  eluz1  9737  uzind4  9795  indstr  9800  supinfneg  9802  infsupneg  9803  infregelbex  9805  indstr2  9816  ublbneg  9820  irrmulap  9855  elpq  9856  elpqb  9857  elrp  9863  mnfltxr  9994  nn0pnfge0  9999  xrltnsym  10001  xrlttr  10003  xrltso  10004  xrlttri3  10005  xrltne  10021  ngtmnft  10025  nmnfgt  10026  xrrebnd  10027  z2ge  10034  xltnegi  10043  xltadd1  10084  xsubge0  10089  xleaddadd  10095  ixxval  10104  elixx1  10105  elioo2  10129  iccid  10133  iccsupr  10174  repos  10178  fzval  10218  elfz1  10221  fzm1  10308  zsupcllemstep  10461  suprzubdc  10468  zsupssdc  10470  qdclt  10477  exbtwnzlemstep  10479  exbtwnzlemex  10481  qbtwnre  10488  qbtwnxr  10489  flval  10504  apbtwnz  10506  modqid2  10585  modqmuladdnn0  10602  exp3val  10775  expge0  10809  expge1  10810  nn0ltexp2  10943  facdiv  10972  facwordi  10974  hashinfom  11012  hashennn  11014  hashunlem  11038  zfz1iso  11076  wrdlen1  11122  fstwrdne0  11124  wrdl1exs1  11177  pfxsuffeqwrdeq  11246  pfxsuff1eqwrdeq  11247  ccats1pfxeq  11262  ccats1pfxeqrex  11263  pfxccatin12lem3  11280  ovshftex  11346  shftfibg  11347  shftfib  11350  shftfn  11351  2shfti  11358  sqrt0rlem  11530  resqrexlemex  11552  rsqrmo  11554  resqrtcl  11556  rersqrtthlem  11557  sqrtsq  11571  cau3lem  11641  caubnd2  11644  maxleim  11732  maxabslemval  11735  maxleast  11740  maxleb  11743  fimaxre2  11754  minmax  11757  xrmaxleim  11771  xrmaxiflemval  11777  xrmaxaddlem  11787  xrminmax  11792  xrbdtri  11803  climi  11814  climeu  11823  climmo  11825  2clim  11828  addcn2  11837  mulcn2  11839  reccn2ap  11840  cn1lem  11841  summodc  11910  zsumdc  11911  fsum3  11914  cvgratz  12059  ntrivcvgap0  12076  prodmodc  12105  zproddc  12106  fprodseq  12110  fprodntrivap  12111  sinltxirr  12288  dvdsabsb  12337  0dvds  12338  alzdvds  12381  dvdsext  12382  fzo0dvdseq  12384  2tp1odd  12411  2teven  12414  divalglemnn  12445  divalglemeunn  12448  divalglemeuneg  12450  bitsinv1lem  12488  gcdval  12496  gcddvds  12500  bezoutlemstep  12534  bezoutlemmain  12535  bezoutlemex  12538  bezoutlemeu  12544  bezoutlemsup  12546  dfgcd3  12547  bezout  12548  dvdsgcd  12549  dfgcd2  12551  dvdssq  12568  uzwodc  12574  nnwofdc  12575  lcmval  12601  lcmcllem  12605  dvdslcm  12607  lcmledvds  12608  lcmgcdlem  12615  lcmdvds  12617  coprmgcdb  12626  coprmdvds2  12631  cncongr1  12641  cncongr2  12642  isprm  12647  dvdsnprmd  12663  dvdsprm  12675  exprmfct  12676  isprm6  12685  prmexpb  12689  prmfac1  12690  rpexp  12691  sqrt2irr  12700  oddpwdclemdc  12711  oddpwdc  12712  sqpweven  12713  2sqpwodd  12714  sqne2sq  12715  nnoddn2prmb  12801  pceu  12834  pczpre  12836  pcdiv  12841  pcdvdsb  12859  difsqpwdvds  12877  pcmpt  12882  pcmptdvds  12884  oddprmdvds  12893  prmpwdvds  12894  infpnlem2  12899  oddennn  12979  evenennn  12980  exmidunben  13013  nninfdclemcl  13035  nninfdclemp1  13037  nninfdc  13040  infpn2  13043  eqgen  13780  zndvds  14629  znleval  14633  comet  15189  metcnpi  15205  metcnpi2  15206  metcnpi3  15207  addcncntoplem  15251  cncfi  15268  elcncf1di  15269  mulcncflem  15297  dedekindeulemuub  15307  dedekindeulemloc  15309  dedekindeulemlu  15311  dedekindeulemeu  15312  dedekindeu  15313  suplociccreex  15314  suplociccex  15315  dedekindicclemuub  15316  dedekindicclemloc  15318  dedekindicclemlu  15320  dedekindicclemeu  15321  dedekindicclemicc  15322  dedekindicc  15323  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemloc  15331  ivthinc  15333  ivthreinc  15335  dich0  15342  ivthdich  15343  limcimo  15355  cnplimclemr  15359  limccnp2lem  15366  limccoap  15368  eldvap  15372  logltb  15564  lgsdir  15730  lgsne0  15733  gausslemma2dlem0i  15752  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  2lgslem2  15787  2lgs  15799  2sqlem6  15815  2sqlem8  15818  2sqlem10  15820  lfgredg2dom  15946  istrl  16129  clwwlkn0  16151  clwwlkext2edg  16164  sbthom  16482  trilpo  16499  trirec0  16500  apdiff  16504  reap0  16514  cndcap  16515  nconstwlpolem  16521  neapmkv  16524  neap0mkv  16525  ltlenmkv  16526