Theorem breq2 4007

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148  ⟨cop 3595   class class class wbr 4003

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  breq12  4008  breq2i  4011  breq2d  4015  nbrne1  4022  brralrspcev  4061  brimralrspcev  4062  pocl  4303  swopolem  4305  swopo  4306  sowlin  4320  sotricim  4323  sotritrieq  4325  seex  4335  frind  4352  wetriext  4576  vtoclr  4674  posng  4698  brcog  4794  brcogw  4796  opelcnvg  4807  dfdmf  4820  breldmg  4833  dfrnf  4868  dmcoss  4896  resieq  4917  dfres2  4959  elimag  4974  elrelimasn  4994  elimasn  4995  intirr  5015  poirr2  5021  poltletr  5029  dffun6f  5229  dffun4f  5232  fun11  5283  brprcneu  5508  fv3  5538  tz6.12c  5545  relelfvdm  5547  funbrfv  5554  fnbrfvb  5556  funfvdm2f  5581  fndmdif  5621  dff3im  5661  fmptco  5682  foeqcnvco  5790  isorel  5808  isocnv  5811  isotr  5816  isopolem  5822  isosolem  5824  f1oiso  5826  f1oiso2  5827  caovordig  6039  caovordg  6041  caovord  6045  caofrss  6106  caoftrn  6107  poxp  6232  tposoprab  6280  ertr  6549  ecopovsym  6630  ecopovtrn  6631  ecopovsymg  6633  ecopovtrng  6634  th3qlem2  6637  domeng  6751  eqeng  6765  snfig  6813  nneneq  6856  nnfi  6871  ssfilem  6874  domfiexmid  6877  dif1enen  6879  diffitest  6886  findcard  6887  findcard2  6888  findcard2s  6889  diffisn  6892  tridc  6898  fimax2gtrilemstep  6899  inffiexmid  6905  unsnfi  6917  fiintim  6927  fisseneq  6930  isbth  6965  supmoti  6991  eqsupti  6994  supubti  6997  suplubti  6998  suplub2ti  6999  supmaxti  7002  supsnti  7003  isotilem  7004  isoti  7005  supisolem  7006  supisoex  7007  cardcl  7179  isnumi  7180  cardval3ex  7183  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidapne  7258  nqtri3or  7394  ltsonq  7396  ltanqg  7398  ltmnqg  7399  ltexnqq  7406  nsmallnqq  7410  subhalfnqq  7412  ltbtwnnqq  7413  prarloclemarch2  7417  nqnq0pi  7436  prcdnql  7482  prcunqu  7483  prnminu  7487  genpcdl  7517  genprndl  7519  genprndu  7520  genpdisj  7521  nqprm  7540  nqprrnd  7541  nqprdisj  7542  nqprloc  7543  nqprlu  7545  nqprl  7549  addnqprlemru  7556  addnqprlemfl  7557  addnqprlemfu  7558  mulnqprlemru  7572  mulnqprlemfl  7573  mulnqprlemfu  7574  1idpru  7589  ltnqpr  7591  ltnqpri  7592  prplnqu  7618  recexprlemelu  7621  recexprlemm  7622  recexprlemloc  7629  recexprlem1ssl  7631  recexprlemss1u  7634  cauappcvgprlemm  7643  cauappcvgprlemopu  7646  cauappcvgprlemupu  7647  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdfu  7652  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem2  7658  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemopu  7669  caucvgprlemupu  7670  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem2  7678  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnbj  7691  caucvgprprlemmu  7693  caucvgprprlemexbt  7704  caucvgprprlemaddq  7706  caucvgprprlem1  7707  caucvgprprlem2  7708  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  suplocexpr  7723  lttrsr  7760  ltsosr  7762  ltasrg  7768  recexgt0sr  7771  mulgt0sr  7776  aptisr  7777  mulextsr1  7779  srpospr  7781  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  caucvgsr  7800  map2psrprg  7803  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  axprecex  7878  axpre-ltwlin  7881  axpre-lttrn  7882  axpre-apti  7883  axpre-ltadd  7884  axpre-mulgt0  7885  axpre-mulext  7886  axcaucvglemcau  7896  axcaucvglemres  7897  axcaucvg  7898  axpre-suploclemres  7899  axpre-suploc  7900  ltxrlt  8021  lttri3  8035  ltne  8040  eqle  8047  ltordlem  8437  reapti  8534  apreim  8558  squeeze0  8859  lbreu  8900  lble  8902  suprleubex  8909  sup3exmid  8912  nnge1  8940  nn2ge  8950  nn1gt1  8951  nnsub  8956  nominpos  9154  nn0ge0  9199  elnnnn0b  9218  nn0ge2m1nn  9234  zdclt  9328  suprzclex  9349  peano2uz2  9358  peano5uzti  9359  dfuzi  9361  uzind  9362  uzind3  9364  eluz1  9530  uzind4  9586  indstr  9591  supinfneg  9593  infsupneg  9594  infregelbex  9596  indstr2  9607  ublbneg  9611  elpq  9646  elpqb  9647  elrp  9653  mnfltxr  9784  nn0pnfge0  9789  xrltnsym  9791  xrlttr  9793  xrltso  9794  xrlttri3  9795  xrltne  9811  ngtmnft  9815  nmnfgt  9816  xrrebnd  9817  z2ge  9824  xltnegi  9833  xltadd1  9874  xsubge0  9879  xleaddadd  9885  ixxval  9894  elixx1  9895  elioo2  9919  iccid  9923  iccsupr  9964  repos  9968  fzval  10008  elfz1  10011  fzm1  10097  exbtwnzlemstep  10245  exbtwnzlemex  10247  qbtwnre  10254  qbtwnxr  10255  flval  10269  apbtwnz  10271  modqid2  10348  modqmuladdnn0  10365  exp3val  10519  expge0  10553  expge1  10554  nn0ltexp2  10685  facdiv  10713  facwordi  10715  hashinfom  10753  hashennn  10755  hashunlem  10779  zfz1iso  10816  ovshftex  10823  shftfibg  10824  shftfib  10827  shftfn  10828  2shfti  10835  sqrt0rlem  11007  resqrexlemex  11029  rsqrmo  11031  resqrtcl  11033  rersqrtthlem  11034  sqrtsq  11048  cau3lem  11118  caubnd2  11121  maxleim  11209  maxabslemval  11212  maxleast  11217  maxleb  11220  fimaxre2  11230  minmax  11233  xrmaxleim  11247  xrmaxiflemval  11253  xrmaxaddlem  11263  xrminmax  11268  xrbdtri  11279  climi  11290  climeu  11299  climmo  11301  2clim  11304  addcn2  11313  mulcn2  11315  reccn2ap  11316  cn1lem  11317  summodc  11386  zsumdc  11387  fsum3  11390  cvgratz  11535  ntrivcvgap0  11552  prodmodc  11581  zproddc  11582  fprodseq  11586  fprodntrivap  11587  dvdsabsb  11812  0dvds  11813  alzdvds  11854  dvdsext  11855  fzo0dvdseq  11857  2tp1odd  11883  2teven  11886  divalglemnn  11917  divalglemeunn  11920  divalglemeuneg  11922  zsupcllemstep  11940  suprzubdc  11947  zsupssdc  11949  gcdval  11954  gcddvds  11958  bezoutlemstep  11992  bezoutlemmain  11993  bezoutlemex  11996  bezoutlemeu  12002  bezoutlemsup  12004  dfgcd3  12005  bezout  12006  dvdsgcd  12007  dfgcd2  12009  dvdssq  12026  uzwodc  12032  nnwofdc  12033  lcmval  12057  lcmcllem  12061  dvdslcm  12063  lcmledvds  12064  lcmgcdlem  12071  lcmdvds  12073  coprmgcdb  12082  coprmdvds2  12087  cncongr1  12097  cncongr2  12098  isprm  12103  dvdsnprmd  12119  dvdsprm  12131  exprmfct  12132  isprm6  12141  prmexpb  12145  prmfac1  12146  rpexp  12147  sqrt2irr  12156  oddpwdclemdc  12167  oddpwdc  12168  sqpweven  12169  2sqpwodd  12170  sqne2sq  12171  nnoddn2prmb  12256  pceu  12289  pczpre  12291  pcdiv  12296  pcdvdsb  12313  difsqpwdvds  12331  pcmpt  12335  pcmptdvds  12337  oddprmdvds  12346  prmpwdvds  12347  infpnlem2  12352  oddennn  12387  evenennn  12388  exmidunben  12421  nninfdclemcl  12443  nninfdclemp1  12445  nninfdc  12448  infpn2  12451  eqgen  13039  comet  13892  metcnpi  13908  metcnpi2  13909  metcnpi3  13910  addcncntoplem  13944  cncfi  13958  elcncf1di  13959  mulcncflem  13983  dedekindeulemuub  13988  dedekindeulemloc  13990  dedekindeulemlu  13992  dedekindeulemeu  13993  dedekindeu  13994  suplociccreex  13995  suplociccex  13996  dedekindicclemuub  13997  dedekindicclemloc  13999  dedekindicclemlu  14001  dedekindicclemeu  14002  dedekindicclemicc  14003  dedekindicc  14004  ivthinclemlopn  14007  ivthinclemlr  14008  ivthinclemuopn  14009  ivthinclemur  14010  ivthinclemloc  14012  ivthinc  14014  limcimo  14027  cnplimclemr  14031  limccnp2lem  14038  limccoap  14040  eldvap  14044  logltb  14188  lgsdir  14329  lgsne0  14332  2sqlem6  14349  2sqlem8  14352  2sqlem10  14354  sbthom  14656  trilpo  14673  trirec0  14674  apdiff  14678  reap0  14688  nconstwlpolem  14694  neapmkv  14697  neap0mkv  14698  ltlenmkv  14699