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

Theorem f1eq2 6800
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 6717 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
21anbi1d 631 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴𝐶 ∧ Fun 𝐹) ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹)))
3 df-f1 6566 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
4 df-f1 6566 . 2 (𝐹:𝐵1-1𝐶 ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  ccnv 5684  Fun wfun 6555  wf 6557  1-1wf1 6558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-fn 6564  df-f 6565  df-f1 6566
This theorem is referenced by:  f1co  6815  f1oeq2  6837  f1eq123d  6840  f10d  6882  brdom2g  8996  brdomgOLD  8998  marypha1lem  9473  fseqenlem1  10064  dfac12lem2  10185  dfac12lem3  10186  ackbij2  10282  iundom2g  10580  hashf1  14496  istrkg3ld  28469  ausgrusgrb  29182  usgr0  29260  uspgr1e  29261  usgrres  29325  usgrexilem  29457  usgr2pthlem  29783  usgr2pth  29784  s2f1  32929  ccatf1  32933  cshf1o  32947  cycpmconjv  33162  cyc3evpm  33170  lindflbs  33407  matunitlindflem2  37624  eldioph2lem2  42772  f1cof1b  47089  fundcmpsurinj  47396  fundcmpsurbijinj  47397  fargshiftf1  47428  f102g  48761  f1mo  48762  aacllem  49320
  Copyright terms: Public domain W3C validator