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

Theorem f1eq2 6547
 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 6472 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
21anbi1d 631 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴𝐶 ∧ Fun 𝐹) ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹)))
3 df-f1 6336 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
4 df-f1 6336 . 2 (𝐹:𝐵1-1𝐶 ↔ (𝐹:𝐵𝐶 ∧ Fun 𝐹))
52, 3, 43bitr4g 316 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ◡ccnv 5530  Fun wfun 6325  ⟶wf 6327  –1-1→wf1 6328 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2813  df-fn 6334  df-f 6335  df-f1 6336 This theorem is referenced by:  f1oeq2  6581  f1eq123d  6584  f10d  6624  brdomg  8497  marypha1lem  8875  fseqenlem1  9428  dfac12lem2  9548  dfac12lem3  9549  ackbij2  9643  iundom2g  9940  hashf1  13800  istrkg3ld  26234  ausgrusgrb  26937  usgr0  27012  uspgr1e  27013  usgrres  27077  usgrexilem  27209  usgr2pthlem  27531  usgr2pth  27532  s2f1  30608  ccatf1  30612  cshf1o  30623  cycpmconjv  30792  cyc3evpm  30800  lindflbs  30949  matunitlindflem2  34930  eldioph2lem2  39495  fundcmpsurinj  43717  fundcmpsurbijinj  43718  fargshiftf1  43749  aacllem  45089
 Copyright terms: Public domain W3C validator