| 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 6717 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
| 2 | 1 | anbi1d 631 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹))) |
| 3 | df-f1 6566 | . 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹)) | |
| 4 | df-f1 6566 | . 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 206 ∧ wa 395 = wceq 1540 ◡ccnv 5684 Fun wfun 6555 ⟶wf 6557 –1-1→wf1 6558 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-fn 6564 df-f 6565 df-f1 6566 |
| This theorem is referenced by: f1co 6815 f1oeq2 6837 f1eq123d 6840 f10d 6882 brdom2g 8996 brdomgOLD 8998 marypha1lem 9473 fseqenlem1 10064 dfac12lem2 10185 dfac12lem3 10186 ackbij2 10282 iundom2g 10580 hashf1 14496 istrkg3ld 28469 ausgrusgrb 29182 usgr0 29260 uspgr1e 29261 usgrres 29325 usgrexilem 29457 usgr2pthlem 29783 usgr2pth 29784 s2f1 32929 ccatf1 32933 cshf1o 32947 cycpmconjv 33162 cyc3evpm 33170 lindflbs 33407 matunitlindflem2 37624 eldioph2lem2 42772 f1cof1b 47089 fundcmpsurinj 47396 fundcmpsurbijinj 47397 fargshiftf1 47428 f102g 48761 f1mo 48762 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |