Theorem f1oeq2 6813

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 6774	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6793	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6545	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6545	. 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 1570  –1-1→wf1 6535  –onto→wfo 6536  –1-1-onto→wf1o 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545

This theorem is used by:  f1oeq23  6815  f1oeq123d  6818  f1oeq2d  6820  resin  6847  isoeq4  7328  breng  8982  f1dmvrnfibi  9330  cnfcom  9701  infxpenc2  10101  fsumf1o  15889  sumsnf  15909  fprodf1o  16113  prodsn  16129  prodsnf  16131  znhash  21864  znunithash  21870  imasf1oxms  24808  wlksnwwlknvbij  30497  clwwlkvbij  30704  eupthp1  30817  derangval  35932  subfacp1lem2a  35945  subfacp1lem3  35947  subfacp1lem5  35949  sumsnd  46042  isuspgrim0lem  48990  isubgr3stgrlem1  49063  usgrexmpl1lem  49118  usgrexmpl2lem  49123  uspgrsprfo  49245  tposf1o  49991