![]() |
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 6017 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1523 Fn wfn 5921 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-fun 5928 df-fn 5929 |
This theorem is referenced by: fnunsn 6036 mptfnf 6053 fnopabg 6055 f1oun 6194 f1oi 6212 f1osn 6214 ovid 6819 curry1 7314 curry2 7317 wfrlem5 7464 wfrlem13 7472 tfrlem10 7528 tfr1 7538 seqomlem2 7591 seqomlem3 7592 seqomlem4 7593 fnseqom 7595 unblem4 8256 r1fnon 8668 alephfnon 8926 alephfplem4 8968 alephfp 8969 cfsmolem 9130 infpssrlem3 9165 compssiso 9234 hsmexlem5 9290 axdclem2 9380 wunex2 9598 wuncval2 9607 om2uzrani 12791 om2uzf1oi 12792 uzrdglem 12796 uzrdgfni 12797 uzrdg0i 12798 hashkf 13159 dmaf 16746 cdaf 16747 prdsinvlem 17571 srg1zr 18575 pws1 18662 frlmphl 20168 ovolunlem1 23311 0plef 23484 0pledm 23485 itg1ge0 23498 itg1addlem4 23511 mbfi1fseqlem5 23531 itg2addlem 23570 qaa 24123 0vfval 27589 xrge0pluscn 30114 bnj927 30965 bnj535 31086 frrlem5 31909 fullfunfnv 32178 neibastop2lem 32480 fourierdlem42 40684 rngcrescrhm 42410 rngcrescrhmALTV 42428 |
Copyright terms: Public domain | W3C validator |