![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqfnfvd | Structured version Visualization version GIF version |
Description: Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.) |
Ref | Expression |
---|---|
eqfnfvd.1 | ⊢ (𝜑 → 𝐹 Fn 𝐴) |
eqfnfvd.2 | ⊢ (𝜑 → 𝐺 Fn 𝐴) |
eqfnfvd.3 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
Ref | Expression |
---|---|
eqfnfvd | ⊢ (𝜑 → 𝐹 = 𝐺) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqfnfvd.3 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) | |
2 | 1 | ralrimiva 3149 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)) |
3 | eqfnfvd.1 | . . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴) | |
4 | eqfnfvd.2 | . . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴) | |
5 | eqfnfv 6779 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) | |
6 | 3, 4, 5 | syl2anc 587 | . 2 ⊢ (𝜑 → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) |
7 | 2, 6 | mpbird 260 | 1 ⊢ (𝜑 → 𝐹 = 𝐺) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∀wral 3106 Fn wfn 6319 ‘cfv 6324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-fv 6332 |
This theorem is referenced by: foeqcnvco 7034 f1eqcocnv 7035 f1eqcocnvOLD 7036 offveq 7410 tfrlem1 7995 updjudhcoinlf 9345 updjudhcoinrg 9346 ackbij2lem2 9651 ackbij2lem3 9652 fpwwe2lem8 10048 seqfeq2 13389 seqfeq 13391 seqfeq3 13416 ccatlid 13931 ccatrid 13932 ccatass 13933 ccatswrd 14021 swrdccat2 14022 pfxid 14037 ccatpfx 14054 pfxccat1 14055 swrdswrd 14058 cats1un 14074 swrdccatin1 14078 swrdccatin2 14082 pfxccatin12 14086 revccat 14119 revrev 14120 cshco 14189 swrdco 14190 seqshft 14436 seq1st 15905 xpsfeq 16828 yonedainv 17523 pwsco1mhm 17988 f1otrspeq 18567 pmtrfinv 18581 symgtrinv 18592 frgpup3lem 18895 ablfac1eu 19188 psgndiflemB 20289 frlmup1 20487 frlmup3 20489 frlmup4 20490 psrlidm 20641 psrridm 20642 psrass1 20643 subrgascl 20737 evlslem1 20754 mavmulass 21154 upxp 22228 uptx 22230 cnextfres1 22673 ovolshftlem1 24113 volsup 24160 dvidlem 24518 dvrec 24558 dveq0 24603 dv11cn 24604 ftc1cn 24646 coemulc 24852 aannenlem1 24924 ulmuni 24987 ulmdv 24998 ostthlem1 26211 nvinvfval 28423 sspn 28519 kbass2 29900 xppreima2 30413 fdifsuppconst 30449 psgnfzto1stlem 30792 cycpmco2 30825 cyc3co2 30832 indpreima 31394 esumcvg 31455 signstres 31955 hgt750lemb 32037 revpfxsfxrev 32475 subfacp1lem4 32543 cvmliftmolem2 32642 msubff1 32916 iprodefisumlem 33085 poimirlem8 35065 poimirlem13 35070 poimirlem14 35071 ftc1cnnc 35129 eqlkr3 36397 cdleme51finvN 37852 metakunt33 39382 ofun 39416 frlmvscadiccat 39440 fsuppind 39456 ismrcd2 39640 rfovcnvf1od 40705 dssmapntrcls 40831 dvconstbi 41038 fsumsermpt 42221 icccncfext 42529 voliooicof 42638 etransclem35 42911 rrxsnicc 42942 ovolval4lem1 43288 zrinitorngc 44624 zrtermorngc 44625 zrtermoringc 44694 1arymaptf1 45056 2arymaptf1 45067 |
Copyright terms: Public domain | W3C validator |