![]() |
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 6216 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1656 Fn wfn 6122 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4147 df-if 4309 df-sn 4400 df-pr 4402 df-op 4406 df-br 4876 df-opab 4938 df-rel 5353 df-cnv 5354 df-co 5355 df-dm 5356 df-fun 6129 df-fn 6130 |
This theorem is referenced by: fnunsn 6235 mptfnf 6252 fnopabg 6254 f1oun 6401 f1oi 6419 f1osn 6421 ovid 7042 curry1 7538 curry2 7541 wfrlem5 7690 wfrlem13 7698 tfrlem10 7754 tfr1 7764 seqomlem2 7817 seqomlem3 7818 seqomlem4 7819 fnseqom 7821 unblem4 8490 r1fnon 8914 alephfnon 9208 alephfplem4 9250 alephfp 9251 cfsmolem 9414 infpssrlem3 9449 compssiso 9518 hsmexlem5 9574 axdclem2 9664 wunex2 9882 wuncval2 9891 om2uzrani 13053 om2uzf1oi 13054 uzrdglem 13058 uzrdgfni 13059 uzrdg0i 13060 hashkf 13419 dmaf 17058 cdaf 17059 prdsinvlem 17885 srg1zr 18890 pws1 18977 frlmphl 20494 ovolunlem1 23670 0plef 23845 0pledm 23846 itg1ge0 23859 itg1addlem4 23872 mbfi1fseqlem5 23892 itg2addlem 23931 qaa 24484 0vfval 28012 xrge0pluscn 30527 bnj927 31381 bnj535 31502 frrlem5 32318 fullfunfnv 32587 neibastop2lem 32888 fourierdlem42 41154 rngcrescrhm 42946 rngcrescrhmALTV 42964 |
Copyright terms: Public domain | W3C validator |