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

Theorem f1oeq2 5452
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 5419 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 5437 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 473 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 5225 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 5225 . 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 1353  1-1wf1 5215  ontowfo 5216  1-1-ontowf1o 5217
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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225
This theorem is referenced by:  f1oeq23  5454  f1oeq123d  5457  f1oeq2d  5459  f1osng  5504  isoeq4  5807  bren  6749  f1dmvrnfibi  6945  summodclem3  11390  summodclem2a  11391  summodc  11393  fsum3  11397  fsumf1o  11400  sumsnf  11419  fprodf1o  11598  prodsnf  11602
  Copyright terms: Public domain W3C validator