![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > feq2 | Structured version Visualization version GIF version |
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
feq2 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq2 6661 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
2 | 1 | anbi1d 631 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))) |
3 | df-f 6567 | . 2 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)) | |
4 | df-f 6567 | . 2 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ⊆ wss 3963 ran crn 5690 Fn wfn 6558 ⟶wf 6559 |
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-fn 6566 df-f 6567 |
This theorem is referenced by: feq23 6720 feq2d 6723 feq2i 6729 f00 6791 f0dom0 6793 f1eq2 6801 fressnfv 7180 poseq 8182 soseq 8183 mapvalg 8875 fsetexb 8903 map0g 8923 ac6sfi 9318 cofsmo 10307 axcc4dom 10479 ac6sg 10526 isghm 19246 isghmOLD 19247 pjdm2 21749 cmpcovf 23415 ulmval 26438 elno2 27714 noreson 27720 measval 34179 isrnmeas 34181 bj-finsumval0 37268 mbfresfi 37653 sn-isghm 42660 dfno2 43418 stoweidlem62 46018 hoidmvval0b 46546 vonioo 46638 vonicc 46641 f102g 48682 f1mo 48683 |
Copyright terms: Public domain | W3C validator |