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

Theorem f1eq2 6666
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 6582 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
21anbi1d 630 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴𝐶 ∧ Fun 𝐹) ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹)))
3 df-f1 6438 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
4 df-f1 6438 . 2 (𝐹:𝐵1-1𝐶 ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  ccnv 5588  Fun wfun 6427  wf 6429  1-1wf1 6430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-fn 6436  df-f 6437  df-f1 6438
This theorem is referenced by:  f1co  6682  f1oeq2  6705  f1eq123d  6708  f10d  6750  brdom2g  8745  brdomgOLD  8747  marypha1lem  9192  fseqenlem1  9780  dfac12lem2  9900  dfac12lem3  9901  ackbij2  9999  iundom2g  10296  hashf1  14171  istrkg3ld  26822  ausgrusgrb  27535  usgr0  27610  uspgr1e  27611  usgrres  27675  usgrexilem  27807  usgr2pthlem  28131  usgr2pth  28132  s2f1  31219  ccatf1  31223  cshf1o  31234  cycpmconjv  31409  cyc3evpm  31417  lindflbs  31574  matunitlindflem2  35774  eldioph2lem2  40583  f1cof1b  44569  fundcmpsurinj  44861  fundcmpsurbijinj  44862  fargshiftf1  44893  f102g  46179  f1mo  46180  aacllem  46505
  Copyright terms: Public domain W3C validator