ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1oeq2 GIF version

Theorem f1oeq2 5528
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 5494 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 5512 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 473 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 5292 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 5292 . 2 (𝐹:𝐵1-1-onto𝐶 ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶))
63, 4, 53bitr4g 223 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1373  1-1wf1 5282  ontowfo 5283  1-1-ontowf1o 5284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188
This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-fn 5288  df-f 5289  df-f1 5290  df-fo 5291  df-f1o 5292
This theorem is referenced by:  f1oeq23  5530  f1oeq123d  5533  f1oeq2d  5535  f1osng  5581  isoeq4  5891  breng  6852  bren  6853  f1dmvrnfibi  7067  summodclem3  11776  summodclem2a  11777  summodc  11779  fsum3  11783  fsumf1o  11786  sumsnf  11805  fprodf1o  11984  prodsnf  11988  znfi  14502  znhash  14503
  Copyright terms: Public domain W3C validator