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

Theorem f1oeq2 6041
 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 6010 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 6025 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 743 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 5811 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 5811 . 2 (𝐹:𝐵1-1-onto𝐶 ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶))
63, 4, 53bitr4g 302 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803 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  df-fo 5810  df-f1o 5811 This theorem is referenced by:  f1oeq23  6043  f1oeq123d  6046  resin  6071  f1osng  6089  f1o2sn  6314  fveqf1o  6457  isoeq4  6470  oacomf1o  7532  bren  7850  f1dmvrnfibi  8133  marypha1lem  8222  oef1o  8478  cnfcomlem  8479  cnfcom  8480  cnfcom2  8482  infxpenc  8724  infxpenc2  8728  pwfseqlem5  9364  pwfseq  9365  summolem3  14292  summo  14295  fsum  14298  fsumf1o  14301  sumsn  14319  prodmolem3  14502  prodmo  14505  fprod  14510  fprodf1o  14515  prodsn  14531  prodsnf  14533  gsumvalx  17093  gsumpropd  17095  gsumpropd2lem  17096  gsumval3lem1  18129  gsumval3  18131  znhash  19726  znunithash  19732  imasf1oxms  22104  cncfcnvcn  22532  wlknwwlknvbij  26268  clwwlkvbij  26329  eupai  26494  eupatrl  26495  eupa0  26501  eupares  26502  eupap1  26503  f1ocnt  28946  derangval  30403  subfacp1lem2a  30416  subfacp1lem3  30418  subfacp1lem5  30420  erdsze2lem1  30439  ismtyval  32769  rngoisoval  32946  lautset  34386  pautsetN  34402  eldioph2lem1  36341  imasgim  36688  sumsnd  38208  f1oeq2d  38356  sumsnf  38636  stoweidlem35  38928  stoweidlem39  38932  wlksnwwlknvbij  41114  clwwlksvbij  41229  eupthp1  41384
 Copyright terms: Public domain W3C validator