![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fneq1i | Structured version Visualization version GIF version |
Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
fneq1i.1 | ⊢ 𝐹 = 𝐺 |
Ref | Expression |
---|---|
fneq1i | ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1i.1 | . 2 ⊢ 𝐹 = 𝐺 | |
2 | fneq1 6646 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1533 Fn wfn 6544 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-fun 6551 df-fn 6552 |
This theorem is referenced by: fnunop 6671 mptfnf 6691 fnopabg 6693 f1oun 6857 f1oi 6876 f1osn 6878 ovid 7562 curry1 8109 curry2 8112 fsplitfpar 8123 frrlem11 8302 wfrlem5OLD 8334 wfrlem13OLD 8342 tfrlem10 8408 tfr1 8418 seqomlem2 8472 seqomlem3 8473 seqomlem4 8474 fnseqom 8476 unblem4 9323 r1fnon 9792 alephfnon 10090 alephfplem4 10132 alephfp 10133 cfsmolem 10295 infpssrlem3 10330 compssiso 10399 hsmexlem5 10455 axdclem2 10545 wunex2 10763 wuncval2 10772 om2uzrani 13953 om2uzf1oi 13954 uzrdglem 13958 uzrdgfni 13959 uzrdg0i 13960 hashkf 14327 dmaf 18041 cdaf 18042 prdsinvlem 19013 srg1zr 20167 pws1 20273 rngcrescrhm 20629 frlmphl 21732 ovolunlem1 25470 0plef 25645 0pledm 25646 itg1ge0 25659 itg1addlem4OLD 25673 mbfi1fseqlem5 25693 itg2addlem 25732 qaa 26303 precsexlem1 28155 precsexlem2 28156 precsexlem3 28157 precsexlem4 28158 precsexlem5 28159 ex-fpar 30344 0vfval 30488 xrge0pluscn 33672 bnj927 34531 bnj535 34652 fullfunfnv 35673 neibastop2lem 35975 fnmptif 44780 fourierdlem42 45675 fcoreslem4 46586 rngcrescrhmALTV 47528 |
Copyright terms: Public domain | W3C validator |