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 6508 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1539 Fn wfn 6413 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-br 5071 df-opab 5133 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-fun 6420 df-fn 6421 |
This theorem is referenced by: fnunop 6531 mptfnf 6552 fnopabg 6554 f1oun 6719 f1oi 6737 f1osn 6739 ovid 7392 curry1 7915 curry2 7918 fsplitfpar 7930 frrlem11 8083 wfrlem5OLD 8115 wfrlem13OLD 8123 tfrlem10 8189 tfr1 8199 seqomlem2 8252 seqomlem3 8253 seqomlem4 8254 fnseqom 8256 unblem4 8999 r1fnon 9456 alephfnon 9752 alephfplem4 9794 alephfp 9795 cfsmolem 9957 infpssrlem3 9992 compssiso 10061 hsmexlem5 10117 axdclem2 10207 wunex2 10425 wuncval2 10434 om2uzrani 13600 om2uzf1oi 13601 uzrdglem 13605 uzrdgfni 13606 uzrdg0i 13607 hashkf 13974 dmaf 17680 cdaf 17681 prdsinvlem 18599 srg1zr 19680 pws1 19770 frlmphl 20898 ovolunlem1 24566 0plef 24741 0pledm 24742 itg1ge0 24755 itg1addlem4OLD 24769 mbfi1fseqlem5 24789 itg2addlem 24828 qaa 25388 ex-fpar 28727 0vfval 28869 xrge0pluscn 31792 bnj927 32649 bnj535 32770 fullfunfnv 34175 neibastop2lem 34476 fourierdlem42 43580 fcoreslem4 44447 rngcrescrhm 45531 rngcrescrhmALTV 45549 |
Copyright terms: Public domain | W3C validator |