Theorem f1oeq3 6167

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 6136	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6151	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 747	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 5933	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 5933	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 303	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523  –1-1→wf1 5923  –onto→wfo 5924  –1-1-onto→wf1o 5925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933

This theorem is referenced by:  f1oeq23  6168  f1oeq123d  6171  f1oeq3d  6172  f1ores  6189  resin  6196  f1osng  6215  f1oresrab  6435  fveqf1o  6597  isoeq5  6611  isoini2  6629  ncanth  6649  oacomf1o  7690  mapsnf1o  7991  bren  8006  xpcomf1o  8090  domss2  8160  isinf  8214  wemapwe  8632  oef1o  8633  cnfcomlem  8634  cnfcom2  8637  cnfcom3  8639  cnfcom3clem  8640  infxpenc  8879  infxpenc2lem1  8880  infxpenc2  8883  fin1a2lem6  9265  hsmexlem1  9286  pwfseqlem5  9523  pwfseq  9524  hashgf1o  12810  axdc4uzlem  12822  sumeq1  14463  fsumss  14500  fsumcnv  14548  prodeq1f  14682  fprodss  14722  fprodcnv  14757  unbenlem  15659  4sqlem11  15706  pwssnf1o  16205  catcisolem  16803  yoniso  16972  gsumvalx  17317  gsumpropd  17319  gsumpropd2lem  17320  xpsmnd  17377  xpsgrp  17581  cayley  17880  cayleyth  17881  gsumval3lem1  18352  gsumval3lem2  18353  gsumcom2  18420  scmatrngiso  20390  m2cpmrngiso  20611  cncfcnvcn  22771  ovolicc2lem4  23334  logf1o2  24441  uspgrf1oedg  26113  wlkiswwlks2lem4  26826  clwwlkvbijOLD  27089  adjbd1o  29072  rinvf1o  29560  eulerpartgbij  30562  eulerpartlemgh  30568  derangval  31275  subfacp1lem2a  31288  subfacp1lem3  31290  subfacp1lem5  31292  mrsubff1o  31538  msubff1o  31580  bj-finsumval0  33277  f1omptsnlem  33313  f1omptsn  33314  poimirlem4  33543  poimirlem9  33548  poimirlem15  33554  ismtyval  33729  ismrer1  33767  rngoisoval  33906  lautset  35686  pautsetN  35702  hvmap1o2  37371  pwfi2f1o  37983  imasgim  37987  uspgrsprfo  42081