Theorem f1oeq2 6809

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 6770	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6789	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 643	. 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 317	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  –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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  f1oeq23  6811  f1oeq123d  6814  f1oeq2d  6816  resin  6843  isoeq4  7318  breng  8948  f1dmvrnfibi  9294  cnfcom  9665  infxpenc2  10002  fsumf1o  15770  sumsnf  15790  fprodf1o  15996  prodsn  16012  prodsnf  16014  znhash  21708  znunithash  21714  imasf1oxms  24646  wlksnwwlknvbij  30257  clwwlkvbij  30464  eupthp1  30567  derangval  35659  subfacp1lem2a  35672  subfacp1lem3  35674  subfacp1lem5  35676  sumsnd  45766  isuspgrim0lem  48678  isubgr3stgrlem1  48751  usgrexmpl1lem  48806  usgrexmpl2lem  48811  uspgrsprfo  48933  tposf1o  49682