Theorem f1oeq3 6129

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 6098	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6113	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 747	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 5895	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 5895	. 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 384   = wceq 1483  –1-1→wf1 5885  –onto→wfo 5886  –1-1-onto→wf1o 5887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895

This theorem is referenced by:  f1oeq23  6130  f1oeq123d  6133  f1oeq3d  6134  f1ores  6151  resin  6158  f1osng  6177  f1oresrab  6395  fveqf1o  6557  isoeq5  6571  isoini2  6589  ncanth  6609  oacomf1o  7645  mapsnf1o  7949  bren  7964  xpcomf1o  8049  domss2  8119  isinf  8173  wemapwe  8594  oef1o  8595  cnfcomlem  8596  cnfcom2  8599  cnfcom3  8601  cnfcom3clem  8602  infxpenc  8841  infxpenc2lem1  8842  infxpenc2  8845  fin1a2lem6  9227  hsmexlem1  9248  pwfseqlem5  9485  pwfseq  9486  hashgf1o  12770  axdc4uzlem  12782  sumeq1  14419  fsumss  14456  fsumcnv  14504  prodeq1f  14638  fprodss  14678  fprodcnv  14713  unbenlem  15612  4sqlem11  15659  pwssnf1o  16158  catcisolem  16756  yoniso  16925  gsumvalx  17270  gsumpropd  17272  gsumpropd2lem  17273  xpsmnd  17330  xpsgrp  17534  cayley  17834  cayleyth  17835  gsumval3lem1  18306  gsumval3lem2  18307  gsumcom2  18374  scmatrngiso  20342  m2cpmrngiso  20563  cncfcnvcn  22724  ovolicc2lem4  23288  logf1o2  24396  uspgrf1oedg  26068  wlkiswwlks2lem4  26758  clwwlksvbij  26922  adjbd1o  28944  rinvf1o  29432  eulerpartgbij  30434  eulerpartlemgh  30440  derangval  31149  subfacp1lem2a  31162  subfacp1lem3  31164  subfacp1lem5  31166  mrsubff1o  31412  msubff1o  31454  bj-finsumval0  33147  f1omptsnlem  33183  f1omptsn  33184  poimirlem4  33413  poimirlem9  33418  poimirlem15  33424  ismtyval  33599  ismrer1  33637  rngoisoval  33776  lautset  35368  pautsetN  35384  hvmap1o2  37054  pwfi2f1o  37666  imasgim  37670  uspgrsprfo  41756