Theorem f1eq2 6800

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

Assertion

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

Proof of Theorem f1eq2

Step	Hyp	Ref	Expression
1		feq2 6717	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6566	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6566	. 2 ⊢ (𝐹:𝐵–1-1→𝐶 ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ^◡ccnv 5684  Fun wfun 6555  ⟶wf 6557  –1-1→wf1 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-fn 6564  df-f 6565  df-f1 6566

This theorem is referenced by:  f1co  6815  f1oeq2  6837  f1eq123d  6840  f10d  6882  brdom2g  8996  brdomgOLD  8998  marypha1lem  9473  fseqenlem1  10064  dfac12lem2  10185  dfac12lem3  10186  ackbij2  10282  iundom2g  10580  hashf1  14496  istrkg3ld  28469  ausgrusgrb  29182  usgr0  29260  uspgr1e  29261  usgrres  29325  usgrexilem  29457  usgr2pthlem  29783  usgr2pth  29784  s2f1  32929  ccatf1  32933  cshf1o  32947  cycpmconjv  33162  cyc3evpm  33170  lindflbs  33407  matunitlindflem2  37624  eldioph2lem2  42772  f1cof1b  47089  fundcmpsurinj  47396  fundcmpsurbijinj  47397  fargshiftf1  47428  f102g  48761  f1mo  48762  aacllem  49320