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 6439 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 = wceq 1533 Fn wfn 6345 |
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 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-br 5060 df-opab 5122 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-fun 6352 df-fn 6353 |
This theorem is referenced by: fnunsn 6459 mptfnf 6478 fnopabg 6480 f1oun 6629 f1oi 6647 f1osn 6649 ovid 7285 curry1 7793 curry2 7796 fsplitfpar 7808 wfrlem5 7953 wfrlem13 7961 tfrlem10 8017 tfr1 8027 seqomlem2 8081 seqomlem3 8082 seqomlem4 8083 fnseqom 8085 unblem4 8767 r1fnon 9190 alephfnon 9485 alephfplem4 9527 alephfp 9528 cfsmolem 9686 infpssrlem3 9721 compssiso 9790 hsmexlem5 9846 axdclem2 9936 wunex2 10154 wuncval2 10163 om2uzrani 13314 om2uzf1oi 13315 uzrdglem 13319 uzrdgfni 13320 uzrdg0i 13321 hashkf 13686 dmaf 17303 cdaf 17304 prdsinvlem 18202 srg1zr 19273 pws1 19360 frlmphl 20919 ovolunlem1 24092 0plef 24267 0pledm 24268 itg1ge0 24281 itg1addlem4 24294 mbfi1fseqlem5 24314 itg2addlem 24353 qaa 24906 ex-fpar 28235 0vfval 28377 xrge0pluscn 31178 bnj927 32035 bnj535 32157 frrlem11 33128 fullfunfnv 33402 neibastop2lem 33703 fourierdlem42 42427 rngcrescrhm 44349 rngcrescrhmALTV 44367 |
Copyright terms: Public domain | W3C validator |