Theorem f1eq2 6580

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542  ^◡ccnv 5534  Fun wfun 6343  ⟶wf 6345  –1-1→wf1 6346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2731  df-fn 6352  df-f 6353  df-f1 6354

This theorem is referenced by:  f1co  6596  f1oeq2  6619  f1eq123d  6622  f10d  6663  brdomg  8577  marypha1lem  8982  fseqenlem1  9536  dfac12lem2  9656  dfac12lem3  9657  ackbij2  9755  iundom2g  10052  hashf1  13921  istrkg3ld  26419  ausgrusgrb  27122  usgr0  27197  uspgr1e  27198  usgrres  27262  usgrexilem  27394  usgr2pthlem  27716  usgr2pth  27717  s2f1  30806  ccatf1  30810  cshf1o  30821  cycpmconjv  30998  cyc3evpm  31006  lindflbs  31158  matunitlindflem2  35429  eldioph2lem2  40195  f1cof1b  44148  fundcmpsurinj  44442  fundcmpsurbijinj  44443  fargshiftf1  44474  aacllem  46005