Theorem breq2 3742

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

Step	Hyp	Ref	Expression
1		opeq2 3524	. . 3 ⊢ (A = B → ⟨𝐶, A⟩ = ⟨𝐶, B⟩)
2	1	eleq1d 2088	. 2 ⊢ (A = B → (⟨𝐶, A⟩ ∈ 𝑅 ↔ ⟨𝐶, B⟩ ∈ 𝑅))
3		df-br 3739	. 2 ⊢ (𝐶𝑅A ↔ ⟨𝐶, A⟩ ∈ 𝑅)
4		df-br 3739	. 2 ⊢ (𝐶𝑅B ↔ ⟨𝐶, B⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 212	1 ⊢ (A = B → (𝐶𝑅A ↔ 𝐶𝑅B))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1228   ∈ wcel 1374  ⟨cop 3353   class class class wbr 3738

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 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-v 2537  df-un 2899  df-sn 3356  df-pr 3357  df-op 3359  df-br 3739

This theorem is referenced by:  breq12  3743  breq2i  3746  breq2d  3750  nbrne1  3755  pocl  4014  swopolem  4016  swopo  4017  sowlin  4031  sotricim  4034  sotritrieq  4036  seex  4040  vtoclr  4315  posng  4339  brcog  4429  brcogw  4431  opelcnvg  4442  dfdmf  4455  breldmg  4468  dfrnf  4502  dmcoss  4528  resieq  4549  dfres2  4585  elimag  4599  elreimasng  4618  elimasn  4619  intirr  4638  poirr2  4644  poltletr  4652  dffun6f  4841  dffun4f  4844  fun11  4892  brprcneu  5096  fv3  5122  tz6.12c  5128  relelfvdm  5130  funbrfv  5137  fnbrfvb  5139  funfvdm2f  5163  fndmdif  5197  dff3im  5237  fmptco  5255  foeqcnvco  5355  isorel  5373  isocnv  5376  isotr  5381  isopolem  5386  isosolem  5388  f1oiso  5390  f1oiso2  5391  caovordig  5589  caovordg  5591  caovord  5595  caofrss  5658  caoftrn  5659  poxp  5775  tposoprab  5817  ertr  6032  ecopovsym  6113  ecopovtrn  6114  ecopovsymg  6116  ecopovtrng  6117  th3qlem2  6120  nqtri3or  6255  ltsonq  6257  ltanqg  6259  ltmnqg  6260  ltexnqq  6266  nsmallnqq  6269  subhalfnqq  6271  ltbtwnnqq  6272  prarloclemarch2  6276  nqnq0pi  6293  prcdnql  6338  prcunqu  6339  prnminu  6343  genpcdl  6374  genprndl  6376  genprndu  6377  genpdisj  6378  nqprm  6397  nqprrnd  6398  nqprdisj  6399  nqprloc  6400  1pr  6404  1idpru  6430  recexprlemelu  6457  recexprlemm  6458  recexprlemloc  6465  recexprlem1ssl  6467  recexprlemss1u  6470  lttrsr  6509  ltsosr  6511  ltasrg  6517  recexsrlem  6520  mulgt0sr  6522  axprecex  6574  axpre-ltwlin  6577  axpre-lttrn  6578  axpre-ltadd  6579  axpre-mulgt0  6580  ltxrlt  6686  ltne  6701  eqle  6705