Theorem f1eq2 6767

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ^◡ccnv 5654  Fun wfun 6527  ⟶wf 6529  –1-1→wf1 6530

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-fn 6536  df-f 6537  df-f1 6538

This theorem is used by:  f1co  6784  f1oeq2  6806  f1eq123d  6809  f10d  6852  brdom2g  8963  marypha1lem  9403  fseqenlem1  10027  dfac12lem2  10147  dfac12lem3  10148  ackbij2  10244  iundom2g  10548  hashf1  14522  ccatf1  14656  matunitlindflem2  22902  istrkg3ld  28802  ausgrusgrb  29625  usgr0  29703  uspgr1e  29704  usgrres  29768  usgrexilem  29900  usgr2pthlem  30228  usgr2pth  30229  s2f1  33389  cshf1o  33402  cycpmconjv  33582  cyc3evpm  33590  lindflbs  33812  eldioph2lem2  43606  f1cof1b  47965  fundcmpsurinj  48309  fundcmpsurbijinj  48310  fargshiftf1  48341  upgrimtrlslem2  48821  f102g  49780  f1mo  49781  aacllem  50772