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

Theorem f1eq2 6135
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 6065 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
21anbi1d 741 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴𝐶 ∧ Fun 𝐹) ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹)))
3 df-f1 5931 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
4 df-f1 5931 . 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 1523  ccnv 5142  Fun wfun 5920  wf 5922  1-1wf1 5923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-fn 5929  df-f 5930  df-f1 5931
This theorem is referenced by:  f1oeq2  6166  f1eq123d  6169  f10d  6208  brdomg  8007  marypha1lem  8380  fseqenlem1  8885  dfac12lem2  9004  dfac12lem3  9005  ackbij2  9103  iundom2g  9400  hashf1  13279  istrkg3ld  25405  ausgrusgrb  26105  usgr0  26180  uspgr1e  26181  usgrres  26245  usgrexilem  26392  usgr2pthlem  26715  usgr2pth  26716  matunitlindflem2  33536  eldioph2lem2  37641  fargshiftf1  41702  aacllem  42875
  Copyright terms: Public domain W3C validator