Theorem f1oeq2 6812

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 6775	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6792	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6543	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6543	. 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 1540  –1-1→wf1 6533  –onto→wfo 6534  –1-1-onto→wf1o 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  f1oeq23  6814  f1oeq123d  6817  f1oeq2d  6819  resin  6845  isoeq4  7318  breng  8973  f1dmvrnfibi  9358  cnfcom  9719  infxpenc2  10041  fsumf1o  15744  sumsnf  15764  fprodf1o  15967  prodsn  15983  prodsnf  15985  znhash  21524  znunithash  21530  imasf1oxms  24433  wlksnwwlknvbij  29895  clwwlkvbij  30099  eupthp1  30202  derangval  35194  subfacp1lem2a  35207  subfacp1lem3  35209  subfacp1lem5  35211  sumsnd  45017  isuspgrim0lem  47873  isubgr3stgrlem1  47945  usgrexmpl1lem  47992  usgrexmpl2lem  47997  uspgrsprfo  48090  tposf1o  48826