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

Theorem f1eq2 6258
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 6188 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
21anbi1d 743 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴𝐶 ∧ Fun 𝐹) ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹)))
3 df-f1 6054 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
4 df-f1 6054 . 2 (𝐹:𝐵1-1𝐶 ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹))
52, 3, 43bitr4g 303 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  ccnv 5265  Fun wfun 6043  wf 6045  1-1wf1 6046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-fn 6052  df-f 6053  df-f1 6054
This theorem is referenced by:  f1oeq2  6289  f1eq123d  6292  f10d  6331  brdomg  8131  marypha1lem  8504  fseqenlem1  9037  dfac12lem2  9158  dfac12lem3  9159  ackbij2  9257  iundom2g  9554  hashf1  13433  istrkg3ld  25559  ausgrusgrb  26259  usgr0  26334  uspgr1e  26335  usgrres  26399  usgrexilem  26546  usgr2pthlem  26869  usgr2pth  26870  matunitlindflem2  33719  eldioph2lem2  37826  fargshiftf1  41887  aacllem  43060
  Copyright terms: Public domain W3C validator