Theorem f1oeq3 6042

Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)

Assertion

Ref	Expression
f1oeq3	⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Proof of Theorem f1oeq3

Step	Hyp	Ref	Expression
1		f1eq3 6011	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6026	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 743	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 5811	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 5811	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 302	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811

This theorem is referenced by:  f1oeq23  6043  f1oeq123d  6046  f1oeq3d  6047  f1ores  6064  resin  6071  f1osng  6089  f1oresrab  6302  fveqf1o  6457  isoeq5  6471  isoini2  6489  ncanth  6509  oacomf1o  7532  mapsnf1o  7835  bren  7850  xpcomf1o  7934  domss2  8004  isinf  8058  wemapwe  8477  oef1o  8478  cnfcomlem  8479  cnfcom2  8482  cnfcom3  8484  cnfcom3clem  8485  infxpenc  8724  infxpenc2lem1  8725  infxpenc2  8728  fin1a2lem6  9110  hsmexlem1  9131  pwfseqlem5  9364  pwfseq  9365  hashgf1o  12632  axdc4uzlem  12644  sumeq1  14267  fsumss  14303  fsumcnv  14346  prodeq1f  14477  fprodss  14517  fprodcnv  14552  unbenlem  15450  4sqlem11  15497  pwssnf1o  15981  catcisolem  16579  equivestrcsetc  16615  yoniso  16748  gsumvalx  17093  gsumpropd  17095  gsumpropd2lem  17096  xpsmnd  17153  xpsgrp  17357  cayley  17657  cayleyth  17658  gsumval3lem1  18129  gsumval3lem2  18130  gsumcom2  18197  scmatrngiso  20161  m2cpmrngiso  20382  cncfcnvcn  22532  ovolicc2lem4  23095  logf1o2  24196  uslgraf1oedg  25888  clwwlkvbij  26329  adjbd1o  28328  rinvf1o  28814  eulerpartgbij  29761  eulerpartlemgh  29767  derangval  30403  subfacp1lem2a  30416  subfacp1lem3  30418  subfacp1lem5  30420  mrsubff1o  30666  msubff1o  30708  bj-finsumval0  32324  f1omptsnlem  32359  f1omptsn  32360  poimirlem4  32583  poimirlem9  32588  poimirlem15  32594  ismtyval  32769  ismrer1  32807  rngoisoval  32946  lautset  34386  pautsetN  34402  hvmap1o2  36072  pwfi2f1o  36684  imasgim  36688  uspgrf1oedg  40403  usgrf1oedg  40434  clwwlksvbij  41229