Theorem f1oeq2 6796

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 6757	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6776	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 641	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6529	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6529	. 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1561  –1-1→wf1 6519  –onto→wfo 6520  –1-1-onto→wf1o 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529

This theorem is referenced by:  f1oeq23  6798  f1oeq123d  6801  f1oeq2d  6803  resin  6830  isoeq4  7305  breng  8937  f1dmvrnfibi  9285  cnfcom  9656  infxpenc2  9979  fsumf1o  15751  sumsnf  15771  fprodf1o  15977  prodsn  15993  prodsnf  15995  znhash  21611  znunithash  21617  imasf1oxms  24550  wlksnwwlknvbij  30109  clwwlkvbij  30316  eupthp1  30419  derangval  35518  subfacp1lem2a  35531  subfacp1lem3  35533  subfacp1lem5  35535  sumsnd  45607  isuspgrim0lem  48516  isubgr3stgrlem1  48589  usgrexmpl1lem  48644  usgrexmpl2lem  48649  uspgrsprfo  48771  tposf1o  49506