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

Theorem f1eq2 6580
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 6496 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
21anbi1d 633 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴𝐶 ∧ Fun 𝐹) ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹)))
3 df-f1 6354 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
4 df-f1 6354 . 2 (𝐹:𝐵1-1𝐶 ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹))
52, 3, 43bitr4g 317 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  ccnv 5534  Fun wfun 6343  wf 6345  1-1wf1 6346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2731  df-fn 6352  df-f 6353  df-f1 6354
This theorem is referenced by:  f1co  6596  f1oeq2  6619  f1eq123d  6622  f10d  6663  brdomg  8577  marypha1lem  8982  fseqenlem1  9536  dfac12lem2  9656  dfac12lem3  9657  ackbij2  9755  iundom2g  10052  hashf1  13921  istrkg3ld  26419  ausgrusgrb  27122  usgr0  27197  uspgr1e  27198  usgrres  27262  usgrexilem  27394  usgr2pthlem  27716  usgr2pth  27717  s2f1  30806  ccatf1  30810  cshf1o  30821  cycpmconjv  30998  cyc3evpm  31006  lindflbs  31158  matunitlindflem2  35429  eldioph2lem2  40195  f1cof1b  44148  fundcmpsurinj  44442  fundcmpsurbijinj  44443  fargshiftf1  44474  aacllem  46005
  Copyright terms: Public domain W3C validator