Theorem f1oeq2 6381

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 6347	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6363	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 624	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6142	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6142	. 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))
6	3, 4, 5	3bitr4g 306	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601  –1-1→wf1 6132  –onto→wfo 6133  –1-1-onto→wf1o 6134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142

This theorem is referenced by:  f1oeq23  6383  f1oeq123d  6386  f1oeq2d  6387  resin  6412  isoeq4  6842  bren  8250  f1dmvrnfibi  8538  cnfcom  8894  infxpenc2  9178  fsumf1o  14861  sumsnf  14880  fprodf1o  15079  prodsn  15095  prodsnf  15097  znhash  20302  znunithash  20308  imasf1oxms  22702  wlksnwwlknvbij  27281  wlksnwwlknvbijOLD  27282  clwwlkvbij  27515  clwwlkvbijOLD  27516  eupthp1  27620  derangval  31748  subfacp1lem2a  31761  subfacp1lem3  31763  subfacp1lem5  31765  sumsnd  40118  uspgrsprfo  42771