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

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

Proof of Theorem f1oeq3
StepHypRef Expression
1 f1eq3 5261 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶1-1𝐴𝐹:𝐶1-1𝐵))
2 foeq3 5279 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
31, 2anbi12d 460 . 2 (𝐴 = 𝐵 → ((𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴) ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵)))
4 df-f1o 5066 . 2 (𝐹:𝐶1-1-onto𝐴 ↔ (𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴))
5 df-f1o 5066 . 2 (𝐹:𝐶1-1-onto𝐵 ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵))
63, 4, 53bitr4g 222 1 (𝐴 = 𝐵 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1299  1-1wf1 5056  ontowfo 5057  1-1-ontowf1o 5058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034  df-f 5063  df-f1 5064  df-fo 5065  df-f1o 5066
This theorem is referenced by:  f1oeq23  5295  f1oeq123d  5298  f1ores  5316  resdif  5323  f1osng  5342  f1oresrab  5517  isoeq5  5638  isoini2  5652  mapsnf1o  6561  bren  6571  xpcomf1o  6648  frechashgf1o  10042  sumeq1  10963  fisumss  11000  fsumcnv  11045  ennnfonelemhf1o  11718  ennnfonelemex  11719
  Copyright terms: Public domain W3C validator