| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > funeq | Structured version Visualization version GIF version | ||
| Description: Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
| Ref | Expression |
|---|---|
| funeq | ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqimss2 4043 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴) | |
| 2 | funss 6585 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵)) | |
| 3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵)) |
| 4 | eqimss 4042 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
| 5 | funss 6585 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴)) | |
| 6 | 4, 5 | syl 17 | . 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴)) |
| 7 | 3, 6 | impbid 212 | 1 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ⊆ wss 3951 Fun wfun 6555 |
| 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-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ss 3968 df-br 5144 df-opab 5206 df-rel 5692 df-cnv 5693 df-co 5694 df-fun 6563 |
| This theorem is referenced by: funeqi 6587 funeqd 6588 fununi 6641 cnvresid 6645 fneq1 6659 funop 7169 funsndifnop 7171 nvof1o 7300 funcnvuni 7954 fiun 7967 elpmg 8883 fundmeng 9072 isfsupp 9405 dfac9 10177 axdc3lem2 10491 frlmphllem 21800 psdmul 22170 oldval 27893 usgredgop 29187 locfinreflem 33839 orvcval 34460 bnj1379 34844 bnj1385 34846 bnj1497 35074 funen1cnv 35102 elfunsg 35917 modelaxreplem1 44995 modelaxreplem2 44996 modelaxrep 44998 funop1 47295 |
| Copyright terms: Public domain | W3C validator |