Theorem f1oeq2 6608

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 6574	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6590	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6365	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6365	. 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 398   = wceq 1536  –1-1→wf1 6355  –onto→wfo 6356  –1-1-onto→wf1o 6357

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 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365

This theorem is referenced by:  f1oeq23  6610  f1oeq123d  6613  f1oeq2d  6614  resin  6639  isoeq4  7076  bren  8521  f1dmvrnfibi  8811  cnfcom  9166  infxpenc2  9451  fsumf1o  15083  sumsnf  15102  fprodf1o  15303  prodsn  15319  prodsnf  15321  znhash  20708  znunithash  20714  imasf1oxms  23102  wlksnwwlknvbij  27690  clwwlkvbij  27895  eupthp1  27998  derangval  32418  subfacp1lem2a  32431  subfacp1lem3  32433  subfacp1lem5  32435  sumsnd  41289  uspgrsprfo  44030