Theorem f1eq2 6770

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 6684	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 642	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6541	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6541	. 2 ⊢ (𝐹:𝐵–1-1→𝐶 ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹))
5	2, 3, 4	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  ^◡ccnv 5660  Fun wfun 6530  ⟶wf 6532  –1-1→wf1 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6539  df-f 6540  df-f1 6541

This theorem is referenced by:  f1co  6787  f1oeq2  6809  f1eq123d  6812  f10d  6855  brdom2g  8950  marypha1lem  9389  fseqenlem1  10004  dfac12lem2  10124  dfac12lem3  10125  ackbij2  10221  iundom2g  10519  hashf1  14490  istrkg3ld  28730  ausgrusgrb  29515  usgr0  29593  uspgr1e  29594  usgrres  29658  usgrexilem  29790  usgr2pthlem  30112  usgr2pth  30113  s2f1  33265  ccatf1  33269  cshf1o  33282  cycpmconjv  33462  cyc3evpm  33470  lindflbs  33692  matunitlindflem2  38268  eldioph2lem2  43492  f1cof1b  47814  fundcmpsurinj  48158  fundcmpsurbijinj  48159  fargshiftf1  48190  upgrimtrlslem2  48670  f102g  49630  f1mo  49631  aacllem  50621