![]() |
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 6838 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) | |
2 | f1oeq3 6839 | . 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 1537 –1-1-onto→wf1o 6562 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-ss 3980 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 |
This theorem is referenced by: f1ofvswap 7326 enfixsn 9120 ackbij2lem2 10277 seqf1o 14081 eulerthlem2 16816 isgim 19293 islmim 21079 fpwrelmapffs 32752 wrdpmcl 32907 1arithidomlem2 33544 1arithidom 33545 hgt750lemg 34648 poimirlem3 37610 poimirlem15 37622 eldioph2lem1 42748 fundcmpsurbijinj 47335 gricushgr 47824 isgrlim 47885 |
Copyright terms: Public domain | W3C validator |