Theorem breq1i 2068

Description: Equality inference for binary relation.

Hypothesis

Ref	Expression
breq1i.1	⊢ A = B

Assertion

Ref	Expression
breq1i	⊢ (ARC ↔ BRC)

Proof of Theorem breq1i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 ⊢ A = B
2		breq1 2065	. 2 ⊢ (A = B → (ARC ↔ BRC))
3	1, 2	ax-mp 6	1 ⊢ (ARC ↔ BRC)

Syntax hints:   ↔ wb 127   = wceq 1091   class class class wbr 2054

This theorem is referenced by:  breq12i 2070  eqbrtr 2076  2dom 3332  0sdom1dom 3420  prfi 3444  imadomg 3616  unxpdomlem 3649  reclem3pr 3952  gt0srpr 3981  mappsrpr 4012  ltpsrpr 4013  map2psrpr 4014  axmulgt0 4086  ltsubadd 4316  addgt0 4323  ltaddpos 4327  ltnegcon2 4333  ltmullem 4337  lesub0 4341  sqgt0 4343  lt0neg1t 4370  le0neg1t 4372  ltdiv23i 4412  lt2sq 4414  nnleltp1t 4448  halfpost 4508  elnn0nn 4593  uzwo3lem2 4615  seqlem2 4663  nn0opthlem1 4722  absnid 4851  ruclem1 4885  ruclem8 4892  cvexch 5760

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063

metamath.org