![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1oeq2 | GIF version |
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
f1oeq2 | ⊢ (A = B → (𝐹:A–1-1-onto→𝐶 ↔ 𝐹:B–1-1-onto→𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1eq2 5031 | . . 3 ⊢ (A = B → (𝐹:A–1-1→𝐶 ↔ 𝐹:B–1-1→𝐶)) | |
2 | foeq2 5046 | . . 3 ⊢ (A = B → (𝐹:A–onto→𝐶 ↔ 𝐹:B–onto→𝐶)) | |
3 | 1, 2 | anbi12d 442 | . 2 ⊢ (A = B → ((𝐹:A–1-1→𝐶 ∧ 𝐹:A–onto→𝐶) ↔ (𝐹:B–1-1→𝐶 ∧ 𝐹:B–onto→𝐶))) |
4 | df-f1o 4852 | . 2 ⊢ (𝐹:A–1-1-onto→𝐶 ↔ (𝐹:A–1-1→𝐶 ∧ 𝐹:A–onto→𝐶)) | |
5 | df-f1o 4852 | . 2 ⊢ (𝐹:B–1-1-onto→𝐶 ↔ (𝐹:B–1-1→𝐶 ∧ 𝐹:B–onto→𝐶)) | |
6 | 3, 4, 5 | 3bitr4g 212 | 1 ⊢ (A = B → (𝐹:A–1-1-onto→𝐶 ↔ 𝐹:B–1-1-onto→𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 = wceq 1242 –1-1→wf1 4842 –onto→wfo 4843 –1-1-onto→wf1o 4844 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-fn 4848 df-f 4849 df-f1 4850 df-fo 4851 df-f1o 4852 |
This theorem is referenced by: f1oeq23 5063 f1oeq123d 5066 f1osng 5110 isoeq4 5387 bren 6164 |
Copyright terms: Public domain | W3C validator |