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

Theorem f1eq2 6010
 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 5940 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
21anbi1d 737 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴𝐶 ∧ Fun 𝐹) ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹)))
3 df-f1 5809 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
4 df-f1 5809 . 2 (𝐹:𝐵1-1𝐶 ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹))
52, 3, 43bitr4g 302 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ◡ccnv 5037  Fun wfun 5798  ⟶wf 5800  –1-1→wf1 5801 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fn 5807  df-f 5808  df-f1 5809 This theorem is referenced by:  f1oeq2  6041  f1eq123d  6044  f10d  6082  brdomg  7851  marypha1lem  8222  fseqenlem1  8730  dfac12lem2  8849  dfac12lem3  8850  ackbij2  8948  iundom2g  9241  hashf1  13098  istrkg3ld  25160  isuslgra  25872  isusgra  25873  ausisusgra  25884  uslgra1  25901  usgra1  25902  cusgraexilem2  25996  2trllemE  26083  constr1trl  26118  fargshiftf1  26165  usgrcyclnl2  26169  4cycl4dv  26195  matunitlindflem2  32576  eldioph2lem2  36342  ausgrusgrb  40395  usgr0  40469  uspgr1e  40470  usgrexi  40661  usgr2pthlem  40969  usgr2pth  40970  aacllem  42356
 Copyright terms: Public domain W3C validator