Theorem f1oeq2 6757

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 6720	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6737	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 638	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6493	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6493	. 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))
6	3, 4, 5	3bitr4g 315	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  –1-1→wf1 6483  –onto→wfo 6484  –1-1-onto→wf1o 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493

This theorem is referenced by:  f1oeq23  6759  f1oeq123d  6762  f1oeq2d  6764  resin  6790  isoeq4  7265  breng  8893  f1dmvrnfibi  9242  cnfcom  9613  infxpenc2  9936  fsumf1o  15677  sumsnf  15697  fprodf1o  15903  prodsn  15919  prodsnf  15921  znhash  21534  znunithash  21540  imasf1oxms  24473  wlksnwwlknvbij  29995  clwwlkvbij  30202  eupthp1  30305  derangval  35404  subfacp1lem2a  35417  subfacp1lem3  35419  subfacp1lem5  35421  sumsnd  45483  isuspgrim0lem  48392  isubgr3stgrlem1  48465  usgrexmpl1lem  48520  usgrexmpl2lem  48525  uspgrsprfo  48647  tposf1o  49382