Theorem f1oeq2 6689

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 6650	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6669	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 630	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6425	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6425	. 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  –1-1→wf1 6415  –onto→wfo 6416  –1-1-onto→wf1o 6417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425

This theorem is referenced by:  f1oeq23  6691  f1oeq123d  6694  f1oeq2d  6696  resin  6721  isoeq4  7171  breng  8700  brenOLD  8702  f1dmvrnfibi  9033  cnfcom  9388  infxpenc2  9709  fsumf1o  15363  sumsnf  15383  fprodf1o  15584  prodsn  15600  prodsnf  15602  znhash  20678  znunithash  20684  imasf1oxms  23551  wlksnwwlknvbij  28174  clwwlkvbij  28378  eupthp1  28481  derangval  33029  subfacp1lem2a  33042  subfacp1lem3  33044  subfacp1lem5  33046  sumsnd  42458  uspgrsprfo  45198