![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > foeq2 | Structured version Visualization version GIF version |
Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
foeq2 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq2 6638 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
2 | 1 | anbi1d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶))) |
3 | df-fo 6546 | . 2 ⊢ (𝐹:𝐴–onto→𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐶)) | |
4 | df-fo 6546 | . 2 ⊢ (𝐹:𝐵–onto→𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 313 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ran crn 5676 Fn wfn 6535 –onto→wfo 6538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2724 df-fn 6543 df-fo 6546 |
This theorem is referenced by: foco 6816 f1oeq2 6819 foeq123d 6823 tposfo 8234 brwdom 9558 brwdom2 9564 canthwdom 9570 cfslb2n 10259 0ramcl 16952 ghmcyg 19758 txcmpb 23139 qtoptopon 23199 fsupprnfi 31901 opidon2OLD 36710 fnfocofob 45773 fullthinc 47619 |
Copyright terms: Public domain | W3C validator |