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

Theorem f1oeq2 6381
 Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq2 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))

Proof of Theorem f1oeq2
StepHypRef Expression
1 f1eq2 6347 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 6363 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 624 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 6142 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 6142 . 2 (𝐹:𝐵1-1-onto𝐶 ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶))
63, 4, 53bitr4g 306 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601  –1-1→wf1 6132  –onto→wfo 6133  –1-1-onto→wf1o 6134 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754 This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142 This theorem is referenced by:  f1oeq23  6383  f1oeq123d  6386  f1oeq2d  6387  resin  6412  isoeq4  6842  bren  8250  f1dmvrnfibi  8538  cnfcom  8894  infxpenc2  9178  fsumf1o  14861  sumsnf  14880  fprodf1o  15079  prodsn  15095  prodsnf  15097  znhash  20302  znunithash  20308  imasf1oxms  22702  wlksnwwlknvbij  27281  wlksnwwlknvbijOLD  27282  clwwlkvbij  27515  clwwlkvbijOLD  27516  eupthp1  27620  derangval  31748  subfacp1lem2a  31761  subfacp1lem3  31763  subfacp1lem5  31765  sumsnd  40118  uspgrsprfo  42771
 Copyright terms: Public domain W3C validator