![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1eq1 | GIF version |
Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
f1eq1 | ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feq1 5082 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | |
2 | cnveq 4558 | . . . 4 ⊢ (𝐹 = 𝐺 → ◡𝐹 = ◡𝐺) | |
3 | 2 | funeqd 4974 | . . 3 ⊢ (𝐹 = 𝐺 → (Fun ◡𝐹 ↔ Fun ◡𝐺)) |
4 | 1, 3 | anbi12d 457 | . 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺))) |
5 | df-f1 4958 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
6 | df-f1 4958 | . 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺)) | |
7 | 4, 5, 6 | 3bitr4g 221 | 1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 = wceq 1285 ◡ccnv 4391 Fun wfun 4947 ⟶wf 4949 –1-1→wf1 4950 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-v 2613 df-un 2987 df-in 2989 df-ss 2996 df-sn 3423 df-pr 3424 df-op 3426 df-br 3807 df-opab 3861 df-rel 4399 df-cnv 4400 df-co 4401 df-dm 4402 df-rn 4403 df-fun 4955 df-fn 4956 df-f 4957 df-f1 4958 |
This theorem is referenced by: f1oeq1 5170 f1eq123d 5174 fun11iun 5200 fo00 5215 tposf12 5940 f1dom2g 6326 f1domg 6328 dom3d 6344 domtr 6355 |
Copyright terms: Public domain | W3C validator |