Theorem breq1i 3345

Description: Equality inference for a 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 3341	. 2 |- (A = B -> (ARC <-> BRC))
3	1, 2	ax-mp 7	1 |- (ARC <-> BRC)

Syntax hints:   <-> wb 163   = wceq 1298   class class class wbr 3338

This theorem is referenced by:  eqbrtri 3356  2dom 5486  0sdom1dom 5618  unxpdomlem 5995  gt0srpr 6339  mappsrpr 6370  ltpsrpr 6371  map2psrpr 6372  pre-axmulgt0 6443  ltsubaddi 6769  ltsubaddiOLD 6770  lesubaddi 6771  addgt0iOLD 6776  ltnegcon2i 6785  lesub0iOLD 6793  msqgt0i 6794  ltmullem 6824  lt0neg1 6857  le0neg1 6859  lt2msqi 7064  reclt1 7081  halfpos 7222  addltmul 7229  elnn0nn 7380  recnz 7403  dfuzi 7414  uzindOLD 7420  uzwo3lem2 7430  seq1lem2 7723  bernneq 7898  bernneqOLD 7899  nn0opthlem1 7914  faclbnd4lem1 8200  bcpasci 8221  cbvsumi 8246  climuz0i 8368  iserzshfti 8404  isum1clim 8458  isumnn0nn 8468  isum0spliti 8478  geoisum1c 8507  cvgratlem2ALT 8510  isupivthi 8552  efseq1ex 8568  dfef2i 8569  efseq0ex 8573  efcl 8574  efcvg 8576  efcvgfsum 8577  reefcli 8579  ef1tllem 8643  eirrlem1 8651  eirrlem4 8654  efcnlem1 8684  ruclem1 8779  ruclem8 8786  bcthlem32 9308  sincosq1sgn 10053  sincosq3sgn 10055  sincosq4sgn 10056  hhbloi 11465  cvexchi 11941  addltmulALT 12018  divalglem1 13697  divalglem6 13701  zgt1b2 13772  isprm2lem 13774  isprm3 13776  unpde2eg2 14406  dfdir2 14639  cntrsetlem 14999  reconnlem3 15448  ufilen 15579  fsumltisumi 15823  fsumleisumi 15826  iccshftr 15857  iccshftl 15859  iccdil 15861  icccntr 15863  pcoass 16085

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339

Copyright terms: Public domain