Theorem f1oeq2 6824

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 6785	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6804	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6554	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6554	. 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  –1-1→wf1 6544  –onto→wfo 6545  –1-1-onto→wf1o 6546

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554

This theorem is used by:  f1oeq23  6826  f1oeq123d  6829  f1oeq2d  6831  resin  6858  isoeq4  7338  breng  8996  f1dmvrnfibi  9344  cnfcom  9714  infxpenc2  10114  fsumf1o  15904  sumsnf  15924  fprodf1o  16128  prodsn  16144  prodsnf  16146  znhash  21879  znunithash  21885  imasf1oxms  24823  wlksnwwlknvbij  30512  clwwlkvbij  30719  eupthp1  30832  derangval  36056  subfacp1lem2a  36069  subfacp1lem3  36071  subfacp1lem5  36073  sumsnd  46185  isuspgrim0lem  49133  isubgr3stgrlem1  49206  usgrexmpl1lem  49261  usgrexmpl2lem  49266  uspgrsprfo  49388  tposf1o  50139