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 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→𝐶)) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |