| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > f1oeq23 | Structured version Visualization version GIF version | ||
| Description: Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.) |
| Ref | Expression |
|---|---|
| f1oeq23 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1oeq2 6837 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) | |
| 2 | f1oeq3 6838 | . 2 ⊢ (𝐶 = 𝐷 → (𝐹:𝐵–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷)) | |
| 3 | 1, 2 | sylan9bb 509 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 –1-1-onto→wf1o 6560 |
| 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-ss 3968 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 |
| This theorem is referenced by: f1ofvswap 7326 enfixsn 9121 ackbij2lem2 10279 seqf1o 14084 eulerthlem2 16819 isgim 19280 islmim 21061 fpwrelmapffs 32745 wrdpmcl 32922 1arithidomlem2 33564 1arithidom 33565 hgt750lemg 34669 poimirlem3 37630 poimirlem15 37642 eldioph2lem1 42771 fundcmpsurbijinj 47397 gricushgr 47886 isgrlim 47949 |
| Copyright terms: Public domain | W3C validator |