![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > feq23d | Structured version Visualization version GIF version |
Description: Equality deduction for functions. (Contributed by NM, 8-Jun-2013.) |
Ref | Expression |
---|---|
feq23d.1 | ⊢ (𝜑 → 𝐴 = 𝐶) |
feq23d.2 | ⊢ (𝜑 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
feq23d | ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd 2827 | . 2 ⊢ (𝜑 → 𝐹 = 𝐹) | |
2 | feq23d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) | |
3 | feq23d.2 | . 2 ⊢ (𝜑 → 𝐵 = 𝐷) | |
4 | 1, 2, 3 | feq123d 6268 | 1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1658 ⟶wf 6120 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-rab 3127 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4875 df-opab 4937 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-fun 6126 df-fn 6127 df-f 6128 |
This theorem is referenced by: nvof1o 6792 axdc4uz 13079 isacs 16665 isfunc 16877 funcres 16909 funcpropd 16913 estrcco 17123 funcestrcsetclem9 17142 fullestrcsetc 17145 fullsetcestrc 17160 1stfcl 17191 2ndfcl 17192 evlfcl 17216 curf1cl 17222 yonedalem3b 17273 intopsn 17607 mhmpropd 17695 pwssplit1 19419 evls1sca 20049 islindf 20519 rrxds 23562 wlkp1 26983 acunirnmpt 30009 cnmbfm 30871 wrdfd 31163 elmrsubrn 31964 poimirlem3 33957 poimirlem28 33982 isrngod 34240 rngosn3 34266 isgrpda 34297 islfld 35138 tendofset 36834 tendoset 36835 mapfzcons 38124 diophrw 38167 refsum2cnlem1 40015 mgmhmpropd 42633 funcringcsetcALTV2lem9 42892 funcringcsetclem9ALTV 42915 aacllem 43444 |
Copyright terms: Public domain | W3C validator |