ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  breq2 Structured version   GIF version

Theorem breq2 3759
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq2 (A = B → (𝐶𝑅A𝐶𝑅B))

Proof of Theorem breq2
StepHypRef Expression
1 opeq2 3541 . . 3 (A = B → ⟨𝐶, A⟩ = ⟨𝐶, B⟩)
21eleq1d 2103 . 2 (A = B → (⟨𝐶, A 𝑅 ↔ ⟨𝐶, B 𝑅))
3 df-br 3756 . 2 (𝐶𝑅A ↔ ⟨𝐶, A 𝑅)
4 df-br 3756 . 2 (𝐶𝑅B ↔ ⟨𝐶, B 𝑅)
52, 3, 43bitr4g 212 1 (A = B → (𝐶𝑅A𝐶𝑅B))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1242   wcel 1390  cop 3370   class class class wbr 3755
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756
This theorem is referenced by:  breq12  3760  breq2i  3763  breq2d  3767  nbrne1  3772  pocl  4031  swopolem  4033  swopo  4034  sowlin  4048  sotricim  4051  sotritrieq  4053  seex  4057  vtoclr  4331  posng  4355  brcog  4445  brcogw  4447  opelcnvg  4458  dfdmf  4471  breldmg  4484  dfrnf  4518  dmcoss  4544  resieq  4565  dfres2  4601  elimag  4615  elreimasng  4634  elimasn  4635  intirr  4654  poirr2  4660  poltletr  4668  dffun6f  4858  dffun4f  4861  fun11  4909  brprcneu  5114  fv3  5140  tz6.12c  5146  relelfvdm  5148  funbrfv  5155  fnbrfvb  5157  funfvdm2f  5181  fndmdif  5215  dff3im  5255  fmptco  5273  foeqcnvco  5373  isorel  5391  isocnv  5394  isotr  5399  isopolem  5404  isosolem  5406  f1oiso  5408  f1oiso2  5409  caovordig  5608  caovordg  5610  caovord  5614  caofrss  5677  caoftrn  5678  poxp  5794  tposoprab  5836  ertr  6057  ecopovsym  6138  ecopovtrn  6139  ecopovsymg  6141  ecopovtrng  6142  th3qlem2  6145  domeng  6169  eqeng  6182  snfig  6227  nnfi  6251  ssfiexmid  6254  nqtri3or  6380  ltsonq  6382  ltanqg  6384  ltmnqg  6385  ltexnqq  6391  nsmallnqq  6395  subhalfnqq  6397  ltbtwnnqq  6398  prarloclemarch2  6402  nqnq0pi  6420  prcdnql  6466  prcunqu  6467  prnminu  6471  genpcdl  6501  genprndl  6503  genprndu  6504  genpdisj  6505  nqprm  6524  nqprrnd  6525  nqprdisj  6526  nqprloc  6527  nqprlu  6529  nqprl  6532  addnqprlemru  6538  addnqprlemfl  6539  addnqprlemfu  6540  1idpru  6566  recexprlemelu  6594  recexprlemm  6595  recexprlemloc  6602  recexprlem1ssl  6604  recexprlemss1u  6607  cauappcvgprlemm  6616  cauappcvgprlemopu  6619  cauappcvgprlemupu  6620  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem2  6631  lttrsr  6670  ltsosr  6672  ltasrg  6678  recexgt0sr  6681  mulgt0sr  6684  aptisr  6685  mulextsr1  6687  axprecex  6744  axpre-ltwlin  6747  axpre-lttrn  6748  axpre-apti  6749  axpre-ltadd  6750  axpre-mulgt0  6751  axpre-mulext  6752  ltxrlt  6862  lttri3  6875  ltne  6880  eqle  6886  reapti  7343  apreim  7367  squeeze0  7631  nnge1  7698  nn2ge  7707  nn1gt1  7708  nnsub  7713  nominpos  7919  nn0ge0  7963  elnnnn0b  7982  nn0ge2m1nn  7998  zdclt  8074  peano2uz2  8101  peano5uzti  8102  dfuzi  8104  uzind  8105  uzind3  8107  eluz1  8233  uzind4  8287  indstr  8292  indstr2  8302  ublbneg  8304  elrp  8340  mnfltxr  8457  nn0pnfge0  8462  xrltnsym  8464  xrlttr  8466  xrltso  8467  xrlttri3  8468  xrltne  8479  ngtmnft  8481  xrrebnd  8482  z2ge  8489  xltnegi  8498  ixxval  8515  elixx1  8516  elioo2  8540  iccid  8544  iccsupr  8585  repos  8589  fzval  8626  elfz1  8629  fzm1  8712  expival  8891  expge0  8925  expge1  8926  sqrt0rlem  9192  sqrtsq  9194
  Copyright terms: Public domain W3C validator