MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1eq2 Structured version   Visualization version   GIF version

Theorem f1eq2 5994
Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1eq2 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))

Proof of Theorem f1eq2
StepHypRef Expression
1 feq2 5925 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
21anbi1d 736 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴𝐶 ∧ Fun 𝐹) ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹)))
3 df-f1 5794 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
4 df-f1 5794 . 2 (𝐹:𝐵1-1𝐶 ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹))
52, 3, 43bitr4g 301 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  ccnv 5026  Fun wfun 5783  wf 5785  1-1wf1 5786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602  df-fn 5792  df-f 5793  df-f1 5794
This theorem is referenced by:  f1oeq2  6025  f1eq123d  6028  f10d  6066  brdomg  7828  marypha1lem  8199  fseqenlem1  8707  dfac12lem2  8826  dfac12lem3  8827  ackbij2  8925  iundom2g  9218  hashf1  13052  istrkg3ld  25104  isuslgra  25665  isusgra  25666  ausisusgra  25677  uslgra1  25694  usgra1  25695  cusgraexilem2  25789  2trllemE  25876  constr1trl  25911  fargshiftf1  25958  usgrcyclnl2  25962  4cycl4dv  25988  matunitlindflem2  32359  eldioph2lem2  36125  ausgrusgrb  40376  usgr0  40450  uspgr1e  40451  usgrexi  40642  usgr2pthlem  40950  usgr2pth  40951  aacllem  42298
  Copyright terms: Public domain W3C validator