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

Theorem f1eq2 6312
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 6238 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
21anbi1d 624 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴𝐶 ∧ Fun 𝐹) ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹)))
3 df-f1 6106 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
4 df-f1 6106 . 2 (𝐹:𝐵1-1𝐶 ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹))
52, 3, 43bitr4g 306 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  ccnv 5311  Fun wfun 6095  wf 6097  1-1wf1 6098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2792  df-fn 6104  df-f 6105  df-f1 6106
This theorem is referenced by:  f1oeq2  6346  f1eq123d  6349  f10d  6389  brdomg  8205  marypha1lem  8581  fseqenlem1  9133  dfac12lem2  9254  dfac12lem3  9255  ackbij2  9353  iundom2g  9650  hashf1  13490  istrkg3ld  25712  ausgrusgrb  26401  usgr0  26477  uspgr1e  26478  usgrres  26542  usgrexilem  26690  usgr2pthlem  27017  usgr2pth  27018  matunitlindflem2  33895  eldioph2lem2  38110  fargshiftf1  42217  aacllem  43349
  Copyright terms: Public domain W3C validator