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

Theorem f1oeq2 6281
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 6250 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 6265 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 749 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 6048 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 6048 . 2 (𝐹:𝐵1-1-onto𝐶 ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  1-1wf1 6038  ontowfo 6039  1-1-ontowf1o 6040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-cleq 2745  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048
This theorem is referenced by:  f1oeq23  6283  f1oeq123d  6286  resin  6311  f1osng  6330  f1o2sn  6563  fveqf1o  6712  isoeq4  6725  oacomf1o  7806  bren  8122  f1dmvrnfibi  8407  marypha1lem  8496  oef1o  8760  cnfcomlem  8761  cnfcom  8762  cnfcom2  8764  infxpenc  9023  infxpenc2  9027  pwfseqlem5  9669  pwfseq  9670  summolem3  14636  summo  14639  fsum  14642  fsumf1o  14645  sumsnf  14664  sumsn  14666  prodmolem3  14854  prodmo  14857  fprod  14862  fprodf1o  14867  prodsn  14883  prodsnf  14885  gsumvalx  17463  gsumpropd  17465  gsumpropd2lem  17466  gsumval3lem1  18498  gsumval3  18500  znhash  20101  znunithash  20107  imasf1oxms  22487  cncfcnvcn  22917  wlksnwwlknvbij  27018  clwwlkvbij  27254  clwwlkvbijOLD  27255  eupthp1  27360  f1ocnt  29860  derangval  31448  subfacp1lem2a  31461  subfacp1lem3  31463  subfacp1lem5  31465  erdsze2lem1  31484  ismtyval  33904  rngoisoval  34081  lautset  35863  pautsetN  35879  eldioph2lem1  37817  imasgim  38164  sumsnd  39676  f1oeq2d  39852  stoweidlem35  40747  stoweidlem39  40751  uspgrsprfo  42258
  Copyright terms: Public domain W3C validator