Theorem f1oeq2 6761

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 6724	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6741	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6497	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6497	. 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 1541  –1-1→wf1 6487  –onto→wfo 6488  –1-1-onto→wf1o 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497

This theorem is referenced by:  f1oeq23  6763  f1oeq123d  6766  f1oeq2d  6768  resin  6794  isoeq4  7264  breng  8890  f1dmvrnfibi  9239  cnfcom  9607  infxpenc2  9930  fsumf1o  15644  sumsnf  15664  fprodf1o  15867  prodsn  15883  prodsnf  15885  znhash  21511  znunithash  21517  imasf1oxms  24431  wlksnwwlknvbij  29930  clwwlkvbij  30137  eupthp1  30240  derangval  35310  subfacp1lem2a  35323  subfacp1lem3  35325  subfacp1lem5  35327  sumsnd  45213  isuspgrim0lem  48081  isubgr3stgrlem1  48154  usgrexmpl1lem  48209  usgrexmpl2lem  48214  uspgrsprfo  48336  tposf1o  49071