Theorem f1eq3 6784

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

Assertion

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

Proof of Theorem f1eq3

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540  ^◡ccnv 5675  Fun wfun 6537  ⟶wf 6539  –1-1→wf1 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-f 6547  df-f1 6548

This theorem is referenced by:  f1oeq3  6823  f1eq123d  6825  tposf12  8242  brdom2g  8957  brdomgOLD  8959  1sdom2dom  9253  pwfseq  10665  f1linds  21690  isusgrs  28849  usgrstrrepe  28925  usgrexilem  29130  tocycval  32703  diaf1oN  40465  f1cof1b  46244