Theorem f1oeq2 6817

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

Step	Hyp	Ref	Expression
1		f1eq2 6780	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6797	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6548	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6548	. 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539  –1-1→wf1 6538  –onto→wfo 6539  –1-1-onto→wf1o 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548

This theorem is referenced by:  f1oeq23  6819  f1oeq123d  6822  f1oeq2d  6824  resin  6850  isoeq4  7322  breng  8976  f1dmvrnfibi  9363  cnfcom  9722  infxpenc2  10044  fsumf1o  15742  sumsnf  15762  fprodf1o  15965  prodsn  15981  prodsnf  15983  znhash  21532  znunithash  21538  imasf1oxms  24447  wlksnwwlknvbij  29857  clwwlkvbij  30061  eupthp1  30164  derangval  35147  subfacp1lem2a  35160  subfacp1lem3  35162  subfacp1lem5  35164  sumsnd  45003  isuspgrim0lem  47844  isubgr3stgrlem1  47906  usgrexmpl1lem  47953  usgrexmpl2lem  47958  uspgrsprfo  48037  tposf1o  48767