Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > f1eq2 | Structured version Visualization version GIF version |
Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
f1eq2 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feq2 6582 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
2 | 1 | anbi1d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹))) |
3 | df-f1 6438 | . 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹)) | |
4 | df-f1 6438 | . 2 ⊢ (𝐹:𝐵–1-1→𝐶 ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ◡ccnv 5588 Fun wfun 6427 ⟶wf 6429 –1-1→wf1 6430 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-cleq 2730 df-fn 6436 df-f 6437 df-f1 6438 |
This theorem is referenced by: f1co 6682 f1oeq2 6705 f1eq123d 6708 f10d 6750 brdom2g 8745 brdomgOLD 8747 marypha1lem 9192 fseqenlem1 9780 dfac12lem2 9900 dfac12lem3 9901 ackbij2 9999 iundom2g 10296 hashf1 14171 istrkg3ld 26822 ausgrusgrb 27535 usgr0 27610 uspgr1e 27611 usgrres 27675 usgrexilem 27807 usgr2pthlem 28131 usgr2pth 28132 s2f1 31219 ccatf1 31223 cshf1o 31234 cycpmconjv 31409 cyc3evpm 31417 lindflbs 31574 matunitlindflem2 35774 eldioph2lem2 40583 f1cof1b 44569 fundcmpsurinj 44861 fundcmpsurbijinj 44862 fargshiftf1 44893 f102g 46179 f1mo 46180 aacllem 46505 |
Copyright terms: Public domain | W3C validator |